diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-24 10:34:39 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-24 10:34:39 +0200 |
| commit | 94311c3a8f5ddcf16dce313d3ddf5d7433d57e42 (patch) | |
| tree | 563dd9fce8e7d935c703c34121bcf7b65dd69166 | |
| parent | 0ca2fe2e616f303665003bc6cf2d89df385f9394 (diff) | |
coq_makefile: use -include rather than include
This fixes bedrock and eliminates warnings.
Thanks Jason Gross for debugging this!
| -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 |