diff options
Diffstat (limited to 'Makefile.devel')
| -rw-r--r-- | Makefile.devel | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index 0595cfa4..4efe9414 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -87,13 +87,18 @@ DEVELRELEASENAMETARGZ = $(DEVELRELEASENAMETAR).gz # Files not kept under cvs to clean away. -FILES_NONCVS = ChangeLog +FILES_NONCVS = ChangeLog TAGS # Where to install a distribution # DISTINSTALLDIR=/usr/local/share/elisp/proofgeneral # value for dcs.ed.ac.uk: DISTINSTALLDIR=/export/local/share/elisp +# Copied from distributed Makefile +ELISP_DIRS=generic lego coq isa +EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done) +ELC=$(EL:.el=.elc) + FORCE: @@ -103,6 +108,14 @@ FORCE: alldist: alldocs +############################################################ +# +# Make tags file +# +tags: $(ELC) + etags $(EL) > TAGS + + ############################################################ # |