diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -54,6 +54,7 @@ FIND_SKIP_DIRS:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' -o \ + -name 'user-contrib' -o \ -name 'coq-makefile' -o \ -name '.opamcache' -o \ -name '.coq-native' \ @@ -137,6 +138,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 +164,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 : |