about summary refs log tree commit diff
path: root/src
diff options
context:
space:
mode:
authorRalf Jung <post@ralfj.de>2023-04-30 22:39:18 +0200
committerRalf Jung <post@ralfj.de>2023-04-30 22:39:18 +0200
commitbbe3a1542e67fad6f8eb5edabb33c22a80fec799 (patch)
tree1b4a68b33a6e66001bd85adc0ff9c1ec2253884e /src
parent697d13084476d8058423b226578a58a8c7d5c86a (diff)
downloadrust-bbe3a1542e67fad6f8eb5edabb33c22a80fec799.tar.gz
rust-bbe3a1542e67fad6f8eb5edabb33c22a80fec799.zip
make it more obvious when the rustc-pull failed
Diffstat (limited to 'src')
-rwxr-xr-xsrc/tools/miri/miri6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/tools/miri/miri b/src/tools/miri/miri
index 1073ff499ba..4be970b398d 100755
--- a/src/tools/miri/miri
+++ b/src/tools/miri/miri
@@ -121,10 +121,10 @@ rustc-pull)
     # Update rust-version file. As a separate commit, since making it part of
     # the merge has confused the heck out of josh in the past.
     echo "$FETCH_COMMIT" > rust-version
-    git commit rust-version -m "Preparing for merge from rustc"
+    git commit rust-version -m "Preparing for merge from rustc" || (echo "FAILED to commit rust-version file, something went wrong"; exit 1)
     # Fetch given rustc commit and note down which one that was
-    git fetch http://localhost:8000/rust-lang/rust.git@$FETCH_COMMIT$JOSH_FILTER.git
-    git merge FETCH_HEAD --no-ff -m "Merge from rustc"
+    git fetch http://localhost:8000/rust-lang/rust.git@$FETCH_COMMIT$JOSH_FILTER.git || (echo "FAILED to fetch new commits, something went wrong"; exit 1)
+    git merge FETCH_HEAD --no-ff -m "Merge from rustc" || (echo "FAILED to merge new commits, something went wrong"; exit 1)
     exit 0
     ;;
 rustc-push)