diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-08-02 13:47:07 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-08-02 13:52:59 +0200 |
| commit | 1f46ff6db53c2ca471d9ea067d0824755b2f34da (patch) | |
| tree | fac80e4ef28e99b205a1699930997b79c23ca292 /Makefile | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Makefile: 'make clean' now immune to the check for binary files without sources
This is a followup of 7d1fc15. Without this fix, you're warned of leftover files,
but even a 'make clean' is then refused, so you cannot get rid of them easily
(apart via a git clean -xfd).
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -137,6 +137,7 @@ endif # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. +ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii ifndef ACCEPT_ALIEN_VO EXISTINGVO:=$(call find, '*.vo') KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) @@ -162,6 +163,7 @@ remove them first, for instance via 'make clean' \ (or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) endif endif +endif # Apart from clean and tags, everything will be done in a sub-call to make # on Makefile.build. This way, we avoid doing here the -include of .d : |