Mirrors/rust
1
0
Fork 0
mirror of https://github.com/rust-lang/rust.git synced 2026-05-08 01:28:18 +03:00
Code Issues Packages Projects Releases Wiki Activity

make it more obvious when the rustc-pull failed

Browse Source
This commit is contained in:
Ralf Jung
2023-04-30 22:39:18 +02:00
parent 697d130844
commit bbe3a1542e
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/tools/miri/miri
+3 -3
View File
@@ -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)