From: Stefano Zacchiroli Date: Thu, 5 May 2005 15:54:53 +0000 (+0000) Subject: added "tags" target to generate vim tags with otags X-Git-Tag: single_binding~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=532cedb4dfaee23bbddffa70801f6abf604bd436;p=helm.git added "tags" target to generate vim tags with otags --- diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index e07de2783..a09775cce 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -80,9 +80,14 @@ METAS/META.helm-%: METAS/meta.helm-%.src for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done echo "}" >> $@ - libraries.ps: .dep.dot dot -Tps -o $@ $< libraries-complete.ps: .alldep.dot dot -Tps -o $@ $< + +tags: TAGS +.PHONY: TAGS +TAGS: + otags -vi -r . +