make './miri toolchain' work even if we cannot write to rustup dir
This commit is contained in:
parent
0c27c2e605
commit
f5aa3131b4
@ -97,7 +97,9 @@ toolchain)
|
||||
CUR_COMMIT=$(rustc +miri --version -v 2>/dev/null | grep "^commit-hash: " | cut -d " " -f 2)
|
||||
if [[ "$CUR_COMMIT" == "$NEW_COMMIT" ]]; then
|
||||
echo "miri toolchain is already at commit $CUR_COMMIT."
|
||||
if [[ "$TOOLCHAIN" != "miri" ]]; then
|
||||
rustup override set miri
|
||||
fi
|
||||
exit 0
|
||||
fi
|
||||
# Install and setup new toolchain.
|
||||
|
Loading…
Reference in New Issue
Block a user