]> matita.cs.unibo.it Git - helm.git/blobdiff - make/make.ml
added support for single target
[helm.git] / make / make.ml
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