diff --git a/remote_run.sh b/remote_run.sh index f701dec2..4ab30752 100755 --- a/remote_run.sh +++ b/remote_run.sh @@ -7,7 +7,7 @@ impure=0 pure_dir="result" impure_dir="build" -while getopts "h:i" opt; do +while getopts "h:id:" opt; do case "$opt" in \?) exit 0 ;;