diff options
author | Michael Pratt <mpratt@google.com> | 2019-10-01 16:44:27 -0700 |
---|---|---|
committer | gVisor bot <gvisor-bot@google.com> | 2019-10-01 16:45:46 -0700 |
commit | 03ce4dd86c9acd6b6148f68d5d2cf025d8c254bb (patch) | |
tree | 1c8b06a565adfa6985501e04b67032f5fc586c21 /scripts/dev.sh | |
parent | 29207cef141983647816b2270fe6419e56630c64 (diff) |
Remove extra --rm
PiperOrigin-RevId: 272324038
Diffstat (limited to 'scripts/dev.sh')
-rwxr-xr-x | scripts/dev.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/dev.sh b/scripts/dev.sh index ee74dcb72..c67003018 100755 --- a/scripts/dev.sh +++ b/scripts/dev.sh @@ -58,7 +58,7 @@ if [[ ${REFRESH} -eq 0 ]]; then echo echo "Runtimes ${RUNTIME} and ${RUNTIME}-d (debug enabled) setup." echo "Use --runtime="${RUNTIME}" with your Docker command." - echo " docker run --rm --runtime="${RUNTIME}" --rm hello-world" + echo " docker run --rm --runtime="${RUNTIME}" hello-world" echo echo "If you rebuild, use $0 --refresh." |