From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 13 Mar 2006 12:48:17 +0000 (+0000)
Subject: added check to not clean the standard library, a confirmation is required
X-Git-Tag: 0.4.95@7852~1608
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=894e5d5d77b474d98c3106533d62e4e5b15f3d93;p=helm.git

added check to not clean the standard library, a confirmation is required
---

diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml
index 151bb0115..d06671dc5 100644
--- a/matita/matitaclean.ml
+++ b/matita/matitaclean.ml
@@ -32,10 +32,35 @@ module TA = GrafiteAst
 
 let clean_suffixes = [ ".moo"; ".lexicon"; ".metadata"; ".xml.gz" ]
 
+let ask_confirmation _ =
+  print_string "
+  You are trying to delete the whole standard library.
+  Since this may be a dangerous operation, you are asked to type
+    
+    yes, I'm sure
+    
+  verbatim and press enter.\n\n> ";
+  flush stdout;
+  let str = input_line stdin in
+  if str = "yes, I'm sure" then 
+    begin
+      print_string "deletion in progess...\n";
+      flush stdout
+    end
+  else 
+    begin
+      print_string "deletion cancelled.\n";
+      flush stdout;
+      exit 1
+    end
+;;
+
 let main () =
   let _ = MatitaInit.initialize_all () in
   match Helm_registry.get_list Helm_registry.string "matita.args" with
   | [ "all" ] ->
+      if Helm_registry.get_bool "matita.system" then
+        ask_confirmation ();
       LibraryDb.clean_owner_environment ();
       let prefixes = 
         HExtlib.filter_map