diff options
| -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 : |