aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:13 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:13 +0000
commitcf6b384b17a66686f31001d8aeb0958f3cfbfbea (patch)
treeaacde4c36529e4b870e6280c966050cc4bac7fba /Makefile
parent3e70ea9c0967725bd320a6387d19cfb9d5a9b7fe (diff)
make otags only relies on otags
but it requires otags-3.12.2 and and ./configure -usecamlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15147 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile15
1 files changed, 1 insertions, 14 deletions
diff --git a/Makefile b/Makefile
index 695de0c53..e8e328e7c 100644
--- a/Makefile
+++ b/Makefile
@@ -236,7 +236,7 @@ devdocclean:
# Emacs tags
###########################################################################
-.PHONY: tags otags
+.PHONY: tags
tags:
echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
@@ -253,19 +253,6 @@ tags:
"--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
-otags:
- echo $(MLIFILES) $(MLSTATICFILES) | sort -r | xargs otags
- echo $(ML4FILES) | sort -r | xargs \
- etags --append --language=none\
- "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
- "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-
-
%.elc: %.el
ifdef COQ_CONFIGURED
echo "(setq load-path (cons \".\" load-path))" > $*.compile