cleanup() {
set -x
+ set +e +o pipefail
kill ${arvboot_PID} ${consume_stdout_PID} ${wb2_PID} ${consume_wb2_stdout_PID}
wait ${arvboot_PID} ${consume_stdout_PID} ${wb2_PID} ${consume_wb2_stdout_PID} || true
if [ "${CLEANUP_ARVADOS_DIR}" -eq "1" ]; then
fi
if [ -f "${WB2_DIR}/public/config.json" ]; then
- echo "ERROR: Cannot run with Workbench2's public/config.json file"
+ echo "ERROR: Please move public/config.json file out of the way"
exit 1
fi