From efc0dd9c2bcd6eb628727f8d9457ce689432326c Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Fri, 11 May 2007 09:12:19 +0000
Subject: [PATCH] Only do a "make check" if the build is optimized.

---
 verify.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/verify.sh b/verify.sh
index d2c2af40..8a1ba3ad 100755
--- a/verify.sh
+++ b/verify.sh
@@ -94,7 +94,12 @@ function build_ledger() {
 
     (cd gdtoa && make) || exit 1
     make || exit 1
-    make fullcheck || exit 1
+
+    if [ "$1" = "--opt" ]; then
+	make check || exit 1
+    else
+	make fullcheck || exit 1
+    fi
 }
 
 # With all of that defined, now build ledger in all its various