aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 8 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 628ad35ca4..99d4611dce 100644
--- a/Makefile
+++ b/Makefile
@@ -61,7 +61,8 @@ FIND_SKIP_DIRS:='(' \
-name 'user-contrib' -o \
-name 'test-suite' -o \
-name '.opamcache' -o \
- -name '.coq-native' \
+ -name '.coq-native' -o \
+ -name 'plugin_tutorial' \
')' -prune -o
define find
@@ -191,7 +192,7 @@ META.coq: META.coq.in
# Cleaning
###########################################################################
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean
clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean
@@ -237,7 +238,7 @@ docclean:
rm -f doc/coq.tex
rm -rf doc/sphinx/_build
-archclean: clean-ide optclean voclean
+archclean: clean-ide optclean voclean plugin-tutorialclean
rm -rf _build
rm -f $(ALLSTDLIB).*
@@ -268,7 +269,7 @@ cleanconfig:
distclean: clean cleanconfig cacheclean timingclean
voclean:
- find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \
+ find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \
-o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} +
find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +
@@ -278,6 +279,9 @@ timingclean:
-o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \
-o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} +
+plugin-tutorialclean:
+ +$(MAKE) -C $(PLUGINTUTO) clean
+
# Ensure that every compiled file around has a known source file.
# This should help preventing weird compilation failures caused by leftover
# compiled files after deleting or moving some source files.