diff options
author | 2002-03-21 13:32:36 +0000 | |
---|---|---|
committer | 2002-03-21 13:32:36 +0000 | |
commit | d1ecaef92c676736d751dbb3e31f74d84cc9f586 (patch) | |
tree | 23aa27962055b712ff48631973a6c66e69121792 /Makefile.devel | |
parent | 572ccbce91f2f2fa266168583364a48393862777 (diff) |
added hook: proof-before-fontify-output-hook
Diffstat (limited to 'Makefile.devel')
-rw-r--r-- | Makefile.devel | 1 |
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) |