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

diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml
index e1546caa7..a2e5b0f33 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