X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaWiki.ml;h=08f683cbf3fa4633411e4bb6ab5214b965efcef7;hb=fa0347cc0a604ba8743da9479117e1f13ab60482;hp=b5dc5ccf76396cef091d592a34e3e61a359b7115;hpb=e5141edaab98baafa31173da8164fa5d87b808c5;p=helm.git

diff --git a/matita/matitaWiki.ml b/matita/matitaWiki.ml
index b5dc5ccf7..08f683cbf 100644
--- a/matita/matitaWiki.ml
+++ b/matita/matitaWiki.ml
@@ -66,13 +66,9 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-      try
-       let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+       let baseuri = GrafiteTypes.get_baseuri grafite_status in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
-      with GrafiteTypes.Option_error("baseuri", "not found") ->
-       (* no baseuri ==> nothing to clean yet *)
-       exit n
 
 let terminate n =
  let terminator = String.make 1 (Char.chr 249) in
@@ -248,10 +244,11 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_string_option
-         (match !grafite_status with
+        GrafiteTypes.get_baseuri 
+           (match !grafite_status with
              [] -> assert false
-           | s::_ -> s) "baseuri" in
+           | s::_ -> s)
+       in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
            ~must_exist:false ~baseuri ~writable:true