diff options
Diffstat (limited to 'evergreen/functions/shared_scons_directory_umount.sh')
| -rwxr-xr-x | evergreen/functions/shared_scons_directory_umount.sh | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/evergreen/functions/shared_scons_directory_umount.sh b/evergreen/functions/shared_scons_directory_umount.sh new file mode 100755 index 00000000000..6d50da0fdae --- /dev/null +++ b/evergreen/functions/shared_scons_directory_umount.sh @@ -0,0 +1,19 @@ +DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)" +. "$DIR/../prelude.sh" + +cd src + +set -o errexit +set -o verbose + +if [ "${disable_shared_scons_cache}" = true ]; then + exit +fi +if [ "${scons_cache_scope}" = "shared" ]; then + if [ "Windows_NT" = "$OS" ]; then + net use X: /delete || true + else + set_sudo + $sudo umount /efs || true + fi +fi |