From 3497354bbf20822ef4fcb5cb7ece872f57f92062 Mon Sep 17 00:00:00 2001 From: Joel Dice Date: Fri, 15 Mar 2013 17:48:47 -0600 Subject: [PATCH] allow extra flags to be passed to make in ci.sh --- test/ci.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/ci.sh b/test/ci.sh index de7a6a6a47..c1863360b2 100755 --- a/test/ci.sh +++ b/test/ci.sh @@ -2,11 +2,11 @@ set -e -make test -make mode=debug test -make process=interpret test +make ${flags} test +make ${flags} mode=debug test +make ${flags} process=interpret test # bootimage and openjdk builds without openjdk-src don't work: if [ -z "${openjdk}" ]; then - make bootimage=true test + make ${flags} bootimage=true test fi -make tails=true continuations=true test +make ${flags} tails=true continuations=true test