From f5aa3131b4d8d2ed54cb3eda084c82c18cb38d36 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 18 Jul 2023 11:25:06 +0200
Subject: [PATCH] make './miri toolchain' work even if we cannot write to
 rustup dir

---
 src/tools/miri/miri | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/tools/miri/miri b/src/tools/miri/miri
index ace3d17ae2a..1bc4e254ad4 100755
--- a/src/tools/miri/miri
+++ b/src/tools/miri/miri
@@ -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."
-        rustup override set miri
+        if [[ "$TOOLCHAIN" != "miri" ]]; then
+            rustup override set miri
+        fi
         exit 0
     fi
     # Install and setup new toolchain.