X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fmatitac.ml;h=83ab74439129e005717d987083b8bdbbb9b2a908;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=e1546caa737c610077502f35e74653545284f19a;hpb=f583b4389d0227ff0da1954af484db7ef1f5fbfc;p=helm.git

diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml
index e1546caa7..83ab74439 100644
--- a/helm/software/matita/matitac.ml
+++ b/helm/software/matita/matitac.ml
@@ -42,12 +42,15 @@ let main_compiler () =
          prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
          prerr_endline ("\nEnter one of these directories and retry");
          exit 1);
-    | [hd] -> 
-      let root, buri, file, target =
-        Librarian.baseuri_of_script ~include_paths:[] hd 
-      in
-      [target], root
-    | _ -> prerr_endline "Only one target (or none) can be specified.";exit 1
+    | hds -> 
+      let roots_and_targets = 
+       List.map (fun (root, buri, file, target) -> root,target)
+        (List.map (Librarian.baseuri_of_script ~include_paths:[]) hds) in
+      let roots,targets = List.split roots_and_targets in
+      let root = List.hd roots in
+      if (List.exists (fun root' -> root' <> root) roots) then
+       (prerr_endline "Only targets in the same root can be specified.";exit 1);
+      targets, root
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
@@ -55,9 +58,9 @@ let main_compiler () =
   (* here we go *)
   if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   if MatitacLib.Make.make root target then 
-    HLog.message "Compilation successful"
+    (HLog.message "Compilation successful"; 0)
   else
-    HLog.message "Compilation failed"
+    (HLog.message "Compilation failed"; 1)
 ;;
 
 let main () =
@@ -66,7 +69,7 @@ let main () =
   if      Pcre.pmatch ~pat:"^matitadep"    bin then Matitadep.main ()
   else if Pcre.pmatch ~pat:"^matitaclean"  bin then Matitaclean.main ()
   else if Pcre.pmatch ~pat:"^matitawiki"   bin then MatitaWiki.main ()
-  else main_compiler ()
+  else exit (main_compiler ())
 ;;
 
 let _ = main ()