aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.devel
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-25 12:48:32 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-25 12:48:32 +0000
commit98ce8cbe37d8206f2e0c08a918997b196eeea3a1 (patch)
tree09d881526d728322bf3bbfd9be85677f9ad0a964 /Makefile.devel
parentceb2e2f49a5b459af44e0be17de155aa2e70562d (diff)
Added ProofGeneral.texi to tags target.
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 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