aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-12 17:46:17 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-12 17:46:17 +0000
commit9a67c4796f10192af5943cdc4e81cac250d956af (patch)
tree20e1aa604c00423d740d312f23b69674daf74598 /Makefile.devel
parentbfb19d7566d8c068ff2caacf8175b189ff514f83 (diff)
Make ordinary dist before develdist, because dist clears build dir... whoops.
Diffstat (limited to 'Makefile.devel')
-rw-r--r--Makefile.devel4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel
index a2e00b57..33615873 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -161,7 +161,7 @@ FILES_NONCVS = TAGS
DISTINSTALLDIR=/export/local/share/elisp
# Copied from distributed Makefile
-ELISP_DIRS=generic lego coq isa isar plastic demoisa hol98
+ELISP_DIRS=generic lego coq isa isar plastic demoisa hol98 af2 twelf
SUBDIRS=$(ELISP_DIRS) etc doc html images
PWD=$(shell pwd)
@@ -394,7 +394,7 @@ develdist:
## Moreover, a link ProofGeneral -> ProofGeneral-<version>
## is made.
##
-release: distclean tag develdist dist
+release: distclean tag dist develdist
mkdir -p $(RELEASEDIR)
cp -pfr $(DISTBUILDIR)/* $(RELEASEDIR)
(cd $(RELEASEDIR); rm -f $(NAME); ln -s $(RELEASENAME) $(NAME))