diff --git a/run_in_docker.sh b/run_in_docker.sh index dd90ea947..2ffafc932 100755 --- a/run_in_docker.sh +++ b/run_in_docker.sh @@ -17,6 +17,7 @@ set -e if [ $# -ne 3 ]; then echo "Usage: run_in_docker.sh " + exit 1 fi dockerfile=$1