aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-19 01:59:32 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-07-19 01:59:32 +0000
commitb4f80e5c06edc2b3f276e1beefe22920a522d54b (patch)
treee0cb515bc7f6fdf48f45fe0aab6e92f206de86df /Makefile.devel
parentbbaea3128cf2ab661356a7c191f057b6f20917ae (diff)
Add todo to tags
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 804ed8b3..b8e660a1 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -219,7 +219,7 @@ alldist: distdocs
# Make tags file
#
tags: $(EL)
- etags $(EL) doc/ProofGeneral.texi doc/PG-adapting.texi > TAGS
+ etags $(EL) todo doc/ProofGeneral.texi doc/PG-adapting.texi > TAGS
@@ -231,7 +231,7 @@ ChangeLog: FORCE
rcs2log -h "dcs.ed.ac.uk" $(DEVELOPERS) | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix
mv ChangeLog ChangeLog.old
cat ChangeLog.prefix ChangeLog.old > ChangeLog
- rm ChangeLog.prefix ChangeLog.old
+# rm ChangeLog.prefix ChangeLog.old
############################################################
#