#!/bin/bash -e
TIMEOUTCMD=`dirname "${BASH_SOURCE[0]}"`/babysitter
+if ! ${TIMEOUTCMD} -h >/dev/null 2>&1; then
+ TIMEOUTCMD=timeout # fall back to timeout if babysitter doesn't work (e.g. python not installed or wrong version)
+fi
+
export MONO_BABYSITTER_LOG_FILE=babysitter_report.json_lines
helptext ()