X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatitac.ml;h=08dab089f6e44516c43b836a433fc20cda8e74ee;hb=d8c17db3c787f3ea964bbcd3b27427ca44b356d0;hp=5c8ea3738f922d8c04cbf56bb33493051434ad52;hpb=c0700c9d9cf3aa044b2f2945a832a6c2eebd5409;p=helm.git diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml index 5c8ea3738..08dab089f 100644 --- a/matita/matita/matitac.ml +++ b/matita/matita/matitac.ml @@ -57,7 +57,7 @@ let main_compiler () = if system_mode then HLog.message "Compiling in system space"; (* here we go *) if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); - if MatitacLib.Make.make root target then + if List.for_all (MatitaEngine.assert_ng ~include_paths:[] ~root) target then (HLog.message "Compilation successful"; 0) else (HLog.message "Compilation failed"; 1) @@ -66,8 +66,7 @@ let main_compiler () = let main () = Sys.catch_break true; let bin = Filename.basename Sys.argv.(0) in - if Pcre.pmatch ~pat:"^matitadep" bin then Matitadep.main () - else if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () + if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () else exit (main_compiler ()) ;;