summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorACSYS <cvc4-devel@cs.nyu.edu>2012-10-26 18:15:32 +0000
committerACSYS <cvc4-devel@cs.nyu.edu>2012-10-26 18:15:32 +0000
commitdbaaa9f285a2bcb5fd7a555e753968972b998f15 (patch)
treecc402ad9d4233283af5cadffad40eadac9ec8748 /Makefile
parent25cb880b2e3cd3f3624f9c2ba399a2a50b4b2da7 (diff)
today's build system fix: sometimes examples weren't built with "make examples"; fixed
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 4ddb97a85..5bbd61b4c 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@
#
builddir = builds
-.PHONY: all install
+.PHONY: all install examples install-examples
all install examples install-examples .DEFAULT:
@if test -d $(builddir); then \
echo cd $(builddir); \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback