diff --git a/src/ci/run.sh b/src/ci/run.sh index b8b1052c41c1..0841e70a6ed2 100755 --- a/src/ci/run.sh +++ b/src/ci/run.sh @@ -128,6 +128,12 @@ if [ ! -z "$SCRIPT" ]; then sh -x -c "$SCRIPT" ret=$? echo "exit code in src/ci/run.sh: $ret" + + echo "tasklist:" + tasklist + echo -n "location of sh: " + where sh + exit $ret else do_make() {