diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-17 13:57:31 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-11 13:54:35 +0100 |
| commit | e098767a05372bf766b7d8e67e4acb623d5b2abf (patch) | |
| tree | 873d9fea655409c45ce3db4043b0c88935ca5e08 /tools | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
Restoring filtering of native files passed to `rm` during `make clean`.
Was lost during the coq_makefile 1 -> 2 translation.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8f79f8a66..32abba0eb 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -286,13 +286,15 @@ ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files -NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ $(VFILES) \ $(GLOBFILES) \ - $(NATIVEFILESTOINSTALL) \ + $(NATIVEFILES) \ $(CMIFILESTOINSTALL) BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ @@ -532,7 +534,7 @@ clean:: $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) @@ -560,7 +562,7 @@ cleanall:: clean archclean:: @# Extension point $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(NATIVEFILES) $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) .PHONY: archclean |