From b49cc15d925bef4c7dd3fc43585c1b14bf1d6a01 Mon Sep 17 00:00:00 2001
From: Peter Bex <address@hidden>
Date: Sat, 14 Jan 2017 21:24:21 +0100
Subject: [PATCH 2/2] Add a workaround for "time" builtin on bash (cygwin)

---
 tests/runtests.sh | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/tests/runtests.sh b/tests/runtests.sh
index 164c1f4..abb8576 100755
--- a/tests/runtests.sh
+++ b/tests/runtests.sh
@@ -87,7 +87,16 @@ SETUP_PREFIX="${SETUP_PREFIX} -e (register-program \"csi\" (make-pathname ${TEST
 TYPESDB=../types.db
 cp $TYPESDB test-repository/types.db
 
-time=`command >/dev/null -v time && echo time || :`
+time=time
+# On some Bash versions (Cygwin), calling the time builtin from a
+# variable breaks, and some systems don't ship with time(1) or a
+# builtin...
+set +e
+$time echo '' > /dev/null 2> /dev/null
+if [ "$?" -eq 127 ]; then
+    time=':'
+fi
+set -e
 compile="../csc -types ${TYPESDB} -ignore-repository ${COMPILE_OPTIONS} -o a.out"
 compile2="../csc -compiler ${CHICKEN} -v -I${TEST_DIR}/.. -L${TEST_DIR}/.. -include-path ${TEST_DIR}/.."
 compile_s="../csc -s -types ${TYPESDB} -ignore-repository ${COMPILE_OPTIONS}"
-- 
2.1.4