modifications to make matita behave reasonably, removed some useless windows

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 60b112d982cca6bf9e6c75ae77d935d6f3114195..b3c0373eb3120d9d326dccfdb174914b48a34654 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -308,12 +308,9 @@ let _ =
       (fun _ ->
         prerr_endline "Still cleaning the library: don't be impatient!"));
    prerr_endline "Matita is cleaning up. Please wait.";
-   try
-    let baseuri =
-     GrafiteTypes.get_string_option
-      (MatitaScript.current ())#grafite_status "baseuri"
-    in
+   let baseuri = 
+     GrafiteTypes.get_baseuri (MatitaScript.current ())#grafite_status
+   in
      LibraryClean.clean_baseuris [baseuri]
-   with GrafiteTypes.Option_error _ -> ()
 
 (* vim:set foldmethod=marker: *)