Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reset #2675

Merged
merged 0 commits into from
Nov 17, 2022
Merged

Reset #2675

merged 0 commits into from
Nov 17, 2022

Conversation

RalfJung
Copy link
Member

This is the Miri history as extracted from current rustc, with the PRs since the last push applied by hand. It is identical to #2673. I think we should force-push Miri to this commit.

@RalfJung
Copy link
Member Author

@Mark-Simulacrum could I ask you again to temporarily disable branch protection in Miri? We ran into a josh bug and I don't know how to repair this without a Miri force-push. (The faulty commit landed in rustc with rust-lang/rust#104456, but we can't force-push there obviously. This way we sync the fault back to Miri and therefore define it to be the correct history.)

I have updated our scripts so in the future we should be able to detect such faulty pushes before we merge them in rustc. I also confirmed that this commit does round-trip properly.

Cc @rust-lang/miri

@RalfJung RalfJung mentioned this pull request Nov 17, 2022
@RalfJung
Copy link
Member Author

RalfJung commented Nov 17, 2022 via email

@RalfJung
Copy link
Member Author

Yes this branch does not contain 218f60e but contains both of its parents. Good.

@Mark-Simulacrum
Copy link
Member

Allowed force push to users with push access.

@RalfJung
Copy link
Member Author

Hm, that does not seem to work...

remote: error: GH006: Protected branch update failed for refs/heads/master.
remote: error: You're not authorized to push to this branch. Visit https://docs.github.com/articles/about-protected-branches/ for more information.
To github.com:rust-lang/miri.git
 ! [remote rejected]   HEAD -> master (protected branch hook declined)
error: failed to push some refs to 'github.com:rust-lang/miri.git'

@Mark-Simulacrum
Copy link
Member

Try again now? I think there was another toggle I needed to hit

@RalfJung RalfJung merged commit 3162b7a into rust-lang:master Nov 17, 2022
@RalfJung RalfJung deleted the reset branch November 17, 2022 15:15
@RalfJung
Copy link
Member Author

Now it worked. :) Thanks! Please protect the branch again.

@Mark-Simulacrum
Copy link
Member

Done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants