ViewManager/ViewManager.py

changeset 2886
dcaebdef6f4a
parent 2769
8cbebde7a984
child 2965
d133c7edd88a
child 3056
9986ec0e559a
--- a/ViewManager/ViewManager.py	Wed Sep 04 19:37:40 2013 +0200
+++ b/ViewManager/ViewManager.py	Thu Sep 05 18:11:19 2013 +0200
@@ -5621,6 +5621,10 @@
         if self.autosaveTimer.isActive():
             self.autosaveTimer.stop()
         
+        # hide search and replace widgets
+        self.__searchWidget.hide()
+        self.__replaceWidget.hide()
+        
     def __editorOpened(self):
         """
         Private slot to handle the editorOpened signal.

eric ide

mercurial