devtools/devctl.py
changeset 8537 e30d0a7f0087
parent 8454 113184eb4e06
child 8544 3d049071957e
--- a/devtools/devctl.py	Fri Sep 07 14:01:59 2012 +0200
+++ b/devtools/devctl.py	Mon Sep 10 14:00:09 2012 +0200
@@ -91,7 +91,7 @@
         if mod.__file__ is None:
             # odd/rare but real
             continue
-        for path in config.vregistry_path():
+        for path in config.appobjects_path():
             if mod.__file__.startswith(path):
                 del sys.modules[name]
                 break