summaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-11-16 00:48:42 +0000
committerMorgan Deters <mdeters@gmail.com>2011-11-16 00:48:42 +0000
commitd514291efafeef479b819af3f905f339c85086fb (patch)
tree88f22153a7fa157e0d02c996aaabed387ab5c56b /config
parent78af7dfd469b43c17c3ad582a094068484955037 (diff)
* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!
* Also some better configure script wording
Diffstat (limited to 'config')
-rw-r--r--config/bindings.m44
1 files changed, 2 insertions, 2 deletions
diff --git a/config/bindings.m4 b/config/bindings.m4
index 416a338da..5306c8c77 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -143,9 +143,9 @@ else
esac
if test "$binding_error" = yes; then
if test "$cvc4_check_for_bindings" = no; then
- AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+ AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built (the preceding few lines should give an indication why this is).])
else
- AC_MSG_WARN([Language binding \`$binding' cannot be built.])
+ AC_MSG_WARN([Language binding \`$binding' cannot be built (the preceding few lines should give an indication why this is).])
fi
else
CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback