aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-13 06:35:08 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-13 06:35:08 +0000
commit8d8fc9d8fb4a28315bb253641654530aad47e1d6 (patch)
tree2cc580ba07f4562a2539de4eace859efbd00cce3 /Makefile.devel
parent34ef9c552876580d7e504b5306eaa3c2d8a441ee (diff)
Added hol98 to distribution.
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel
index 2da9c01d..605c6fda 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -113,7 +113,7 @@ TAR=tar
DEVELMAKE=make -f Makefile.devel
# Files not to include the distribution area or tarball
-NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel Makefile.xemacs doc/notes.txt doc/ProofGeneral.dvi doc/ProofGeneralPortrait.eps* images/*.xcf images/notes.txt images/gimp images/Makefile plastic/ hol98/
+NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel Makefile.xemacs doc/notes.txt doc/ProofGeneral.dvi doc/ProofGeneralPortrait.eps* images/*.xcf images/notes.txt images/gimp images/Makefile plastic/
# Files not to include in the ordinary distribution tarball, but left
# in the server's copy of the distribution.