X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita.ml;h=b3c0373eb3120d9d326dccfdb174914b48a34654;hb=fa0347cc0a604ba8743da9479117e1f13ab60482;hp=60b112d982cca6bf9e6c75ae77d935d6f3114195;hpb=e5141edaab98baafa31173da8164fa5d87b808c5;p=helm.git

diff --git a/matita/matita.ml b/matita/matita.ml
index 60b112d98..b3c0373eb 100644
--- 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: *)