diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-28 10:05:36 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-28 10:05:36 +0200 |
| commit | c2281e8c3b5103e49b7108a48259d18558b72f57 (patch) | |
| tree | b402f0fbc040fa938e4e431fc5ec81d079af1bc3 /Makefile.build | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
| parent | 7d1fc1501dd89e6e72c07a36e60ef027b0ae2746 (diff) | |
Merge PR #852: Makefile: fails if some .vo or .cm* file has no source
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 e3316df91..7961092fa 100644 --- a/Makefile.build +++ b/Makefile.build @@ -151,7 +151,7 @@ endif # 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) |