Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / matitac.ml

diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml
index 5d0ed9a3512528c8a45886606efd1131dd45677e..a2e5b0f33ec6ad61f799227d0977886cf844ed52 100644 (file)
--- 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
@@ -61,6 +64,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 ()