1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel
index 0d5198c9..27e9756b 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -168,8 +168,8 @@ alldist:	distdocs
 #
 # Make tags file
 #
-tags:	$(ELC)
-	etags $(EL) > TAGS
+tags:	$(EL)
+	etags $(EL) doc/ProofGeneral.texi > TAGS