ViewManager/ViewManager.py

changeset 3261
b8fee972444b
parent 3207
6cf664694e3c
child 3321
ad3a75d3d870
--- a/ViewManager/ViewManager.py	Wed Feb 05 19:09:29 2014 +0100
+++ b/ViewManager/ViewManager.py	Sat Feb 08 20:09:58 2014 +0100
@@ -4543,7 +4543,8 @@
         filenames = []
         for editor in self.editors:
             fn = editor.getFileName()
-            if fn is not None and fn not in filenames:
+            if fn is not None and fn not in filenames and os.path.exists(fn):
+                # only return names of existing files
                 filenames.append(fn)
         
         return filenames

eric ide

mercurial