aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 8d9b657d1..b2aab69ac 100644
--- a/Makefile
+++ b/Makefile
@@ -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 :