diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-13 23:51:28 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-13 23:51:28 +0100 |
| commit | a48be9cd3c9e57606e52c9a5eebb1d02b65fdf66 (patch) | |
| tree | 748d10bb4f9f1d4e83efa74f6ef007d9f9a7e932 /tools | |
| parent | 2c2a08083bc535397359299690d0bfb3523a9ee1 (diff) | |
| parent | e098767a05372bf766b7d8e67e4acb623d5b2abf (diff) | |
Merge PR #6175: Restoring filtering of native files passed to `rm` during `make clean`.
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 7fd942908..6e87e67bb 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -289,13 +289,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) \ @@ -535,7 +537,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) @@ -563,7 +565,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 |