Small interface improvement: selecting something in the proof does not

unload any more the current sequent.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ff93962131671546631ed081eaca21a5df7e5624..8d63437c4b1e62a02d92b22f22eaf2b7f567da4e 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2167,7 +2167,6 @@ object
   (* signal handlers here *)
   ignore(output#connect#selection_changed
    (function elem ->
-     notebook#proofw#unload ;
      choose_selection output elem ;
      !focus_and_proveit_set_sensitive true
    )) ;