projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
0e18d60
)
link TAGS file into builds/ directory, when built. Resolves bug #195
author
Morgan Deters
<mdeters@gmail.com>
Mon, 13 Sep 2010 17:27:15 +0000
(17:27 +0000)
committer
Morgan Deters
<mdeters@gmail.com>
Mon, 13 Sep 2010 17:27:15 +0000
(17:27 +0000)
Makefile.builds.in
patch
|
blob
|
history
diff --git
a/Makefile.builds.in
b/Makefile.builds.in
index 3f5b93b03c338eec9d275f3f20d12146feaf1a70..83183e4a386102f0022be5fe21a652eb09acc6de 100644
(file)
--- a/
Makefile.builds.in
+++ b/
Makefile.builds.in
@@
-91,6
+91,12
@@
check test units regress: all
regress%: all
(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
+TAGS tags:
+ (cd $(CURRENT_BUILD) && $(MAKE) $@)
+ ln -sf $(CURRENT_BUILD)/TAGS .
+
+.PHONY: TAGS tags
+
# any other target than the default doesn't do the extra stuff above
%:
(cd $(CURRENT_BUILD) && $(MAKE) $@)