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 /API/API.mli | |
| 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 'API/API.mli')
0 files changed, 0 insertions, 0 deletions