matitac now automatically cleans a non empty baseuri

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c2b9a7e93615d6120784a0f1dfdf34bf30fdfe0b..821602dcecfd3d591d40b5baf95127b435b84746 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -337,7 +337,7 @@ let eval_executable guistuff status user_goal parsed_text script ex =
         (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitacleanLib.is_empty u) then
+            if not (ML.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition"