From b06c6719c86a6ffc5a09470ba1f275b21a8c7646 Mon Sep 17 00:00:00 2001
From: David Capello <davidcapello@gmail.com>
Date: Fri, 29 Apr 2011 22:02:14 -0300
Subject: [PATCH] Fix problem closing the last "normal" editor (because the
 existence of the new "mini" editor).

---
 src/modules/editors.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/modules/editors.cpp b/src/modules/editors.cpp
index 5296d749e..8f70f9880 100644
--- a/src/modules/editors.cpp
+++ b/src/modules/editors.cpp
@@ -428,8 +428,13 @@ void close_editor(Editor* editor)
   JWidget parent_box = view->getParent(); // Box or panel
   JWidget other_widget;
 
-  // You can't remove all editors.
-  if (editors.size() == 1)
+  // You can't remove all (normal) editors.
+  int normalEditors = 0;
+  for (EditorList::iterator it = editors.begin(); it != editors.end(); ++it) {
+    if (it->getType() == EditorItem::Normal)
+      normalEditors++;
+  }
+  if (normalEditors == 1) // In this case we avoid to remove the last normal editor
     return;
 
   // Deselect the editor.