File tree 1 file changed +10
-2
lines changed 1 file changed +10
-2
lines changed Original file line number Diff line number Diff line change @@ -117,11 +117,13 @@ rustc-pull)
117
117
if [ -z " $FETCH_COMMIT " ]; then
118
118
FETCH_COMMIT=$( git ls-remote https://github.com/rust-lang/rust/ HEAD | cut -f 1)
119
119
fi
120
+ # Update rust-version file. As a separate commit, since making it part of
121
+ # the merge has confused the heck out of josh in the past.
122
+ echo " $FETCH_COMMIT " > rust-version
123
+ git commit rust-version -m " Preparing for merge from rustc"
120
124
# Fetch given rustc commit and note down which one that was
121
125
git fetch http://localhost:8000/rust-lang/rust.git@$FETCH_COMMIT$JOSH_FILTER .git
122
- echo " $FETCH_COMMIT " > rust-version # do this *before* merging as merging will fail in case of conflicts
123
126
git merge FETCH_HEAD --no-ff -m " Merge from rustc"
124
- git commit rust-version --amend -m " Merge from rustc"
125
127
exit 0
126
128
;;
127
129
rustc-push)
@@ -158,6 +160,12 @@ rustc-push)
158
160
cd " $MIRIDIR "
159
161
echo " Pushing Miri changes..."
160
162
git push http://localhost:8000/$USER /rust.git$JOSH_FILTER .git HEAD:$BRANCH
163
+ # Do a round-trip check to make sure the push worked as expected.
164
+ git fetch http://localhost:8000/$USER /rust.git@$JOSH_FILTER .git $BRANCH
165
+ if [[ $( git rev-parse HEAD) != $( git rev-parse FETCH_HEAD) ]]; then
166
+ echo " ERROR: Josh created a non-roundtrip push! Do NOT merge this into rustc!"
167
+ exit 1
168
+ fi
161
169
exit 0
162
170
;;
163
171
many-seeds)
You can’t perform that action at this time.
0 commit comments