diff --git a/scripts/dev_cli.sh b/scripts/dev_cli.sh index 4e0882e65..effe282b3 100755 --- a/scripts/dev_cli.sh +++ b/scripts/dev_cli.sh @@ -226,6 +226,11 @@ cmd_build() { } ;; "--debug") { build="debug"; } ;; "--release") { build="release"; } ;; + "--runtime") + shift + DOCKER_RUNTIME="$1" + export DOCKER_RUNTIME + ;; "--libc") shift [[ "$1" =~ ^(musl|gnu)$ ]] ||