From 1acce08d9a3fa02ffd42a8981198bd06aab4c65d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 13 Mar 2006 12:48:17 +0000
Subject: [PATCH] added check to not clean the standard library, a confirmation
 is required

---
 helm/software/matita/matitaclean.ml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/helm/software/matita/matitaclean.ml b/helm/software/matita/matitaclean.ml
index 151bb0115..d06671dc5 100644
--- a/helm/software/matita/matitaclean.ml
+++ b/helm/software/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 
-- 
2.39.2