diff options
Diffstat (limited to 'tools/CoqMakefile.in')
| -rw-r--r-- | tools/CoqMakefile.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fdcd2ed79..5231899c6 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -526,10 +526,10 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) - include $(ALLDFILES) + -include $(ALLDFILES) else ifeq ($(MAKECMDGOALS),) - include $(ALLDFILES) + -include $(ALLDFILES) endif endif |