aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik.martin-dorel@irit.fr>2017-01-13 08:42:13 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-01-13 08:42:34 +0100
commit9568a34f665a6f3dca06271ffd6e914d9bd2a5ad (patch)
tree248d6f7503ccf13e819d484309f7c318aea223cf /tools/coq_makefile.ml
parentaa21c209f85f37b3d16ff499bbeac15e967bf78f (diff)
Properly remove aux files in subdirectories (bug #5089).
The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux.
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eab909f5b..b7dd5f2a1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -390,7 +390,7 @@ let clean sds sps =
let () =
if !some_vfile then
let () = print "cleanall:: clean\n" in
- print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in
+ print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in
print "archclean::\n";
print "\trm -f *.cmx *.o\n";
List.iter