]> matita.cs.unibo.it Git - helm.git/commitdiff
added support for single target
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Jan 2008 09:55:23 +0000 (09:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 4 Jan 2008 09:55:23 +0000 (09:55 +0000)
make/main.ml
make/make.ml
make/make.mli

index df20a35f2eefa5aa2eed28252cf10ab6e6fbb2f3..0b9cf949aeddd8d5017ff8bae0d4a1f7f10edd88 100644 (file)
@@ -31,4 +31,4 @@ let deps = [
   ]
 ;;
 
-M.make deps;;
+M.make deps (Array.to_list Sys.argv);;
index c243d793515727fdb0c30bae9f8c7548625ac2e7..5a0dc85ce3207933f6a6f56e65c5be75dbb12933 100644 (file)
@@ -97,7 +97,26 @@ module Make = functor (F:Format) -> struct
        make (compiled@List.map fst todo) deps)
   ;;
 
-  let make deps = make [] deps
+  let rec purge_unwanted_roots wanted deps =
+    let roots, rest = 
+       List.partition 
+         (fun (t,d) ->
+           not (List.exists (fun (_,d1) -> List.mem t d1) deps))
+         deps
+    in
+    let newroots = List.filter (fun (t,_) -> List.mem t wanted) roots in
+    if newroots = roots then
+      deps
+    else
+      purge_unwanted_roots wanted (newroots @ rest)
+  ;;
+
+  let make deps targets = 
+    if targets = [] then 
+      make [] deps
+    else
+      make [] (purge_unwanted_roots targets deps)
+  ;;
 
 end
   
index 8830a8319fbee31d06720be7a6ab713777ef35c4..5346c82e7e27ce84ae69edf93790deeb5de8d52c 100644 (file)
@@ -14,5 +14,7 @@ module type Format =
 module Make :
   functor (F : Format) ->
     sig
-      val make : (F.source_object * F.source_object list) list -> unit
+      (* make [deps] [targets], targets = [] means make all *)
+      val make : (F.source_object * F.source_object list) list ->
+                 F.source_object list ->  unit
     end