aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-23 17:23:15 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-11-23 17:23:15 +0000
commit22bf378285c1028cf60a214d8c511b63dd7e63dd (patch)
tree5a46c6341b7a3debab4f4035fb86417547f2cb04 /Makefile.devel
parent5bf11bcf69c8e10e6057fca9c5bed142b602bcd4 (diff)
Include pdf doc in distribution area, though.
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 22c26ef6..7108fc0f 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -106,7 +106,7 @@ TAR=tar
DEVELMAKE=make -f Makefile.devel
# Files not to include the distribution area or tarball
-NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt doc/ProofGeneral.dvi doc/ProofGeneral.eps* doc/ProofGeneral.pdf images/*.xcf images/notes.txt images/gimp images/Makefile html/notes.txt Makefile.xemacs plastic/
+NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt doc/ProofGeneral.dvi doc/ProofGeneral.eps* images/*.xcf images/notes.txt images/gimp images/Makefile Makefile.xemacs plastic/
# Files not to include in the ordinary distribution tarball, but left
# in the server's copy of the distribution.