diff options
| -rwxr-xr-x | src/tools/miri/miri | 6 |
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) |