From b4f80e5c06edc2b3f276e1beefe22920a522d54b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 19 Jul 2002 01:59:32 +0000
Subject: Add todo to tags

---
 Makefile.devel | 4 ++--
 1 file 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
 
 ############################################################
 #
-- 
cgit v1.2.3