From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 7 Jul 2005 09:40:02 +0000 (+0000)
Subject: Bug fixed: no .moo can be generated if the status is <> No_proof
X-Git-Tag: V_0_7_1~31
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ccee7ed50388a3953ce3cae38b5c524b152d92b2;p=helm.git

Bug fixed: no .moo can be generated if the status is <> No_proof
---

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 540a839dd..8e16be52c 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -67,9 +67,10 @@ let clean_current_baseuri status =
 
 let ask_and_save_moo_if_needed parent fname status = 
   let save () =
-    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
-  in
-  if (MatitaScript.instance ())#eos then
+    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+  if (MatitaScript.instance ())#eos &&
+     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+  then
     begin
       let mooname = 
         MatitaMisc.obj_file_of_script fname