From ccee7ed50388a3953ce3cae38b5c524b152d92b2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jul 2005 09:40:02 +0000 Subject: [PATCH] Bug fixed: no .moo can be generated if the status is <> No_proof --- helm/matita/matitaGui.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 -- 2.39.2