devtools/devctl.py
branchstable
changeset 7752 df91baa5b837
parent 7745 1013c31bfbee
child 7990 a673d1d9a738
--- a/devtools/devctl.py	Fri Aug 19 10:53:23 2011 +0200
+++ b/devtools/devctl.py	Fri Aug 19 14:25:06 2011 +0200
@@ -88,6 +88,9 @@
             continue
         if not hasattr(mod, '__file__'):
             continue
+        if mod.__file__ is None:
+            # odd/rare but real
+            continue
         for path in config.vregistry_path():
             if mod.__file__.startswith(path):
                 del sys.modules[name]