diff --git a/run_tests b/run_tests index c1d45db2c..557831506 100755 --- a/run_tests +++ b/run_tests @@ -30,4 +30,11 @@ export REFINE_QUICK_AND_DIRTY=1 cd ${DIR} default="ASpec ExecSpec ASpec_ARM ExecSpec_ARM AInvs HaskellKernel BaseRefine Refine" -python ./misc/regression/run_tests.py ${@:-${default}} $([ -z ${bamboo_planKey} ] || echo $default) +if [ "${bamboo_l4v_regression_identifier}" == "test board" ] +then + bamboo_args=$(echo "$@" | ( [ -z "${bamboo_l4v_regression_options}" ] && cat - || sed 's/'"${bamboo_l4v_regression_options}"'//')) + echo "python ./misc/regression/run_tests.py ${bamboo_args} $default" + python ./misc/regression/run_tests.py ${bamboo_args} $default +else + python ./misc/regression/run_tests.py ${@:-${default}} $([ -z ${bamboo_planKey} ] || echo $default) +fi