Useless GrafiteTypes.get_baseuri removed.

[helm.git] / helm / software / matita / matitaWiki.ml

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index b52e75741f04b11fb25d9cc08b304aa420bc6cb0..30c7fc9eaf954a9306d0c6c3c0b9884538aa4d85 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -64,7 +64,7 @@ let clean_exit n =
   match !grafite_status with
      [] -> exit n
    | grafite_status::_ ->
-       let baseuri = GrafiteTypes.get_baseuri grafite_status in
+       let baseuri = grafite_status#baseuri in
        LibraryClean.clean_baseuris ~verbose:false [baseuri];
        exit n
 
@@ -239,10 +239,9 @@ let main () =
     else
      begin
        let baseuri =
-        GrafiteTypes.get_baseuri 
-           (match !grafite_status with
-             [] -> assert false
-           | s::_ -> s)
+        (match !grafite_status with
+           [] -> assert false
+         | s::_ -> s)#baseuri
        in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri