From 1c496f7b3e9f69da2b9a6072dc4c94fb841601ab Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Jun 2003 16:53:31 +0000
Subject: [PATCH] The "Save proof" menu item is now activated when a finished
 proof is reopened.

---
 helm/gTopLevel/gTopLevel.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index d71162d1e..0f2f73c28 100644
--- 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
-- 
2.39.2