Safely replace tilde characters with user's home path

pathmissing · pathmissing · commit cb40371a4a93 · 2017-09-26T11:16:41.000+02:00
diff --git a/setup-mac.sh b/setup-mac.sh
@@ -189,6 +189,8 @@ if [[ $1 == "--workspace-dir"* ]]
 	fi
 fi
 
+WORKSPACE_DIR="${WORKSPACE_DIR/#\~/$HOME}"
+
 echo ""
 echo '   ____ _____  ____  ________  ______   _____  _____(_)___  '
 echo '  / __ `/ __ \/ __ \/ ___/ _ \/ ___/ | / / _ \/ ___/ / __ \ '
