X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitac.ml;h=f52db24a6bcb72fad797b6b061c8b430ab33857b;hb=3c8a3783837bf7773437b12a089b8edf93879b5d;hp=199b041576550d2a1b952dd96e5ef2112087238d;hpb=4a62bde42e3655a7829b9281d9b9057dc32c0471;p=helm.git

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 199b04157..f52db24a6 100644
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -87,31 +87,34 @@ let dump f =
 (* compiler ala pascal/java using make *)
 let main_compiler () =
   MatitaInit.initialize_all ();
+  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   (* targets and deps *)
   let targets = Helm_registry.get_list Helm_registry.string "matita.args" in
-  let deps, target = 
+  let target, root = 
     match targets with
     | [] ->
       (match Librarian.find_roots_in_dir (Sys.getcwd ()) with
-      | [x] -> 
-         Make.load_deps_file (Filename.dirname x ^ "/depends"), []
+      | [x] -> [], x
       | [] -> 
          HLog.error "No targets and no root found"; exit 1
       | roots -> 
          HLog.error ("Too many roots found, move into one and retry: "^
            String.concat ", " roots);exit 1);
     | [hd] -> 
-      let root, buri, file, target = Librarian.baseuri_of_script hd in
-      HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'");
-      Make.load_deps_file (root ^ "/depends"), [target]
+      let root, buri, file, target =
+        Librarian.baseuri_of_script ~include_paths:[] hd 
+      in
+      [target], root
     | _ -> HLog.error "Only one target (or none) can be specified.";exit 1
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
   if system_mode then HLog.message "Compiling in system space";
-  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   (* here we go *)
-  MatitacLib.Make.make deps target
+  if MatitacLib.Make.make root target then 
+    HLog.message "Compilation successful"
+  else
+    HLog.message "Compilation failed"
 ;;
 
 let main () =