summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
commitda178a880e3ace820b41d38b191d3785b82991f5 (patch)
tree6356ab3164a5ad629f4161dc6c44ead74edc2937 /Makefile
parente4282ea99c664d8d58067bee199cbbcf881b60d5 (diff)
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile9
1 files changed, 4 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index 6854de92..6873d80c 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile 12063 2009-04-08 15:38:39Z herbelin $
+# $Id: Makefile 13182 2010-06-23 09:18:18Z notin $
# Makefile for Coq
@@ -24,8 +24,6 @@
# by Emacs' next-error.
###########################################################################
-export SHELL:=/bin/bash
-
export FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
@@ -183,9 +181,10 @@ docclean:
rm -f doc/*/*.ps doc/*/*.pdf
rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
rm -f doc/stdlib/html/*.html
- rm -f doc/refman/euclid.ml{,i} doc/refman/heapsort.ml{,i}
+ rm -f doc/refman/euclid.ml doc/refman/euclid.mli
+ rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
rm -f doc/common/version.tex
- rm -f doc/refman/*.eps doc/refman/Reference-Manual.html
+ rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/*.eps doc/refman/Reference-Manual.html
rm -f doc/coq.tex
rm -f doc/refman/styles.hva doc/refman/cover.html