From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Jan 2008 17:35:11 +0000 (+0000)
Subject: Matitac now accepts multiple targets :-) (but only in the same root :-(
X-Git-Tag: make_still_working~5658
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6010a5725c95faf03d3f9031203717517582d086;p=helm.git

Matitac now accepts multiple targets :-) (but only in the same root :-(
---

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