aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-03-27 09:29:00 +0100
committerGuillaume Melquiond2015-03-27 09:29:16 +0100
commit0da60299fa3abd4a84c7c673fa8f9ed202c84188 (patch)
tree4dd598d9af52244e8c5df629b7a0316d2c67f39e
parent924a6e99f85aa0d70d42e753d6901b067ebf8f1d (diff)
Properly handle extra "clean" targets with coq_makefile.
-rw-r--r--tools/coq_makefile.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index e2bca2acfb..72735e900f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -536,9 +536,13 @@ let include_dirs (inc_ml,inc_i,inc_r) =
List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n";
end
+let double_colon = ["clean"; "cleanall"; "archclean"]
+
let custom sps =
let pr_path (file,dependencies,is_phony,com) =
- print file; print ": "; print dependencies; print "\n";
+ print file;
+ print (if List.mem file double_colon then ":: " else ": ");
+ print dependencies; print "\n";
if com <> "" then (print "\t"; print com; print "\n");
print "\n"
in