aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2002-03-21 13:32:36 +0000
committerGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2002-03-21 13:32:36 +0000
commitd1ecaef92c676736d751dbb3e31f74d84cc9f586 (patch)
tree23aa27962055b712ff48631973a6c66e69121792 /Makefile.devel
parent572ccbce91f2f2fa266168583364a48393862777 (diff)
added hook: proof-before-fontify-output-hook
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.devel b/Makefile.devel
index 722585fa..fb8ffec6 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -107,6 +107,7 @@ FULLVERSION=$(VERSION)
# NB: CVS tags can't have points in them.
# Substitute points for hyphens.
CVS_VERSION=$(shell echo $(FULLVERSION) | sed 's/\./-/g')
+NOCVS=yes
# Name of tar file and RPM file.
RELEASENAME = $(NAME)-$(VERSION)