diff -r e200f9084c5d -r 8fead6686d1c ViewManager/ViewManager.py --- a/ViewManager/ViewManager.py Fri Nov 04 17:00:01 2011 +0100 +++ b/ViewManager/ViewManager.py Fri Nov 04 17:38:51 2011 +0100 @@ -3098,6 +3098,7 @@ fn = editor.getFileName() # remove the window + editor.parent().shutdownTimer() self._removeView(editor) self.editors.remove(editor)