diff options
author | Fabricio Voznika <fvoznika@google.com> | 2019-09-18 16:54:29 -0700 |
---|---|---|
committer | gVisor bot <gvisor-bot@google.com> | 2019-09-18 16:56:01 -0700 |
commit | a1f84469218d148b1f8210370cb08677b0d74f49 (patch) | |
tree | cdf4202e618fde5bdb06d9cd030af9310aa7a1cf /scripts | |
parent | c98e7f0d19478ca57ba8c96444f225784035321e (diff) |
Fix dev.sh --refresh to create target dir
PiperOrigin-RevId: 269921234
Diffstat (limited to 'scripts')
-rwxr-xr-x | scripts/dev.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/scripts/dev.sh b/scripts/dev.sh index 64151c558..ee74dcb72 100755 --- a/scripts/dev.sh +++ b/scripts/dev.sh @@ -63,6 +63,7 @@ if [[ ${REFRESH} -eq 0 ]]; then echo "If you rebuild, use $0 --refresh." else + mkdir -p "$(dirname ${RUNSC_BIN})" cp -f ${OUTPUT} "${RUNSC_BIN}" echo |