From e098767a05372bf766b7d8e67e4acb623d5b2abf Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 17 Nov 2017 13:57:31 +0100 Subject: Restoring filtering of native files passed to `rm` during `make clean`. Was lost during the coq_makefile 1 -> 2 translation. --- tools/CoqMakefile.in | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'tools') 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 -- cgit v1.2.3