The "Save proof" menu item is now activated when a finished proof is reopened.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index d71162d1e5b3b058e89519444f8a930e7938a299..0f2f73c281740a39ef386991b15c560051421bb8 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1653,7 +1653,8 @@ let open_ () =
        Some (uri, metasenv, bo, ty) ;
       ProofEngine.goal := None ;
       refresh_goals notebook ;
-      refresh_proof output
+      refresh_proof output ;
+      !save_set_sensitive true
    with
       InvokeTactics.RefreshSequentException e ->
        output_html outputhtml