X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatitaclean.ml;h=a3183c16110fdeb03e273b3f55caac0baa1f08f9;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=d9f603652e334cd63e266cc56f7beba1a26f015c;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git diff --git a/helm/software/matita/matitaclean.ml b/helm/software/matita/matitaclean.ml index d9f603652..a3183c161 100644 --- a/helm/software/matita/matitaclean.ml +++ b/helm/software/matita/matitaclean.ml @@ -80,7 +80,8 @@ let clean_all () = ignore (Sys.command ("find " ^ xmldir ^ " -type d -exec rmdir -p {} \\; 2> /dev/null"))) - prefixes + prefixes; + ignore (Sys.command ("rm -rf " ^ Helm_registry.get "matita.basedir")) ;; let main () = @@ -111,12 +112,10 @@ let main () = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin - HLog.error (sprintf "File %s defines a bad baseuri: %s" - suri u); + if Librarian.is_uri u then u else begin + HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); exit 1 - end else - u + end in uri::uris_to_remove) [] files in