diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-15 22:26:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-15 22:26:10 +0000 |
commit | ba84f4ca24d075eddafc93a3dd00d8484e351e0e (patch) | |
tree | a9825cb636ad45019127d922dcba00b4368e8753 /Makefile.builds.in | |
parent | a8ae064eb9ee7175e83eee29d03459b22aa158ef (diff) |
fix for "make examples"
Diffstat (limited to 'Makefile.builds.in')
-rw-r--r-- | Makefile.builds.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in index 249a5e380..f97bf56b8 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -81,7 +81,7 @@ am__v_relink_1 = : # configuration) CVC4_BINARIES = cvc4 pcvc4 -.PHONY: _default_build_ all +.PHONY: _default_build_ all examples _default_build_: all all: # build the current build profile @@ -223,5 +223,5 @@ doc-prereq: +(cd $(CURRENT_BUILD) && for dir in `find . -name Makefile | xargs grep -l BUILT_SOURCES`; do (cd `dirname "$$dir"`; (cat Makefile; echo 'doc-prereq: $$(BUILT_SOURCES)') | $(MAKE) -f- doc-prereq); done) # any other target than the default doesn't do the extra stuff above -%: +examples %: +(cd $(CURRENT_BUILD) && $(MAKE) $@) |