Useless GrafiteTypes.get_baseuri removed.

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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index e9965c4ca130748e0aaf493ad5b93994616142e1..1b4cc5a3cd495042c550710f699a84b1685229ba 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -333,7 +333,7 @@ let _ =
         prerr_endline "Still cleaning the library: don't be impatient!"));
    prerr_endline "Matita is cleaning up. Please wait.";
    let baseuri = 
-     GrafiteTypes.get_baseuri (MatitaScript.current ())#grafite_status
+    (MatitaScript.current ())#grafite_status#baseuri
    in
      LibraryClean.clean_baseuris [baseuri]