diff options
| author | Pierre Letouzey | 2017-07-03 16:37:25 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-07-05 09:29:49 +0200 |
| commit | 7d1fc1501dd89e6e72c07a36e60ef027b0ae2746 (patch) | |
| tree | 5399573ea50eb98822d97dc02a3fcf19397984d3 /Makefile.build | |
| parent | 35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff) | |
Makefile: fails if some .vo or .cm* file has no source
This should help preventing weird compilation failures due to leftover
object files after deleting or moving some source files
By the way:
- use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason
for the suggestion)
- rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more
than version control stuff nowadays
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 0dafde9977..ed1959cff1 100644 --- a/Makefile.build +++ b/Makefile.build @@ -85,7 +85,7 @@ include Makefile.dev ## provides the 'printers' and 'revision' rules # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) -include $(DEPENDENCIES) |