aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-03 23:08:39 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-03 23:08:39 +0000
commit35f05f9f85e02ff7f03f73d884983289c5f4bebb (patch)
treeb5b025076941b9cbc902102d904247e33ac76670 /Makefile.devel
parent1a70304eb6a283abeae1df8c0ed12da34a60d6e4 (diff)
Separate profiling from testing
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel5
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel
index dca47219..a9e9e881 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -213,6 +213,9 @@ tags: $(EL) $(TAGS_EXTRAS)
test.%:
if [ -f "$*/$*-autotest.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-autotest.el -f eval-current-buffer; then echo "Autotests for $* run successfully on `date`"; else cat $*/.autotest.log; echo "Autotests for $* ran with failures on `date`"; exit 1; fi; fi
+profile.%:
+ if [ -f "$*/$*-profiling.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-profiling.el -f eval-current-buffer; then echo "Profiling for $* run successfully on `date`"; else echo "Profiling for $* ran with failures on `date`"; exit 1; fi; cat $*/.profile.log; fi
+
testall.%:
for prover in ${PROVERS}; do $(MAKE) test.$$prover EMACS=$*; done
@@ -251,7 +254,7 @@ devclean: FORCE
#
distclean: devclean clean
@echo "***** CLEANING UP ALL JUNK FILES ****"
- find . \( -name '*~' -o -name '#*#' -o -name '\.\#*' \) -print | xargs rm -f
+ find . \( -name '*~' -o -name '#*#' -o -name '\.\#*' -o -name '\.*\.log' \) -print | xargs rm -f
(cd doc; $(MAKE) distclean)
############################################################