Skip to content

rustup for retag rename #956

New issue

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

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

Already on GitHub? # to your account

Merged
merged 3 commits into from
Sep 18, 2019
Merged

rustup for retag rename #956

merged 3 commits into from
Sep 18, 2019

Conversation

RalfJung
Copy link
Member

This is the Miri side of rust-lang/rust#64503. Do not force-push!

@RalfJung
Copy link
Member Author

@bors r+

@bors
Copy link
Contributor

bors commented Sep 18, 2019

📌 Commit d610d9d has been approved by RalfJung

bors added a commit that referenced this pull request Sep 18, 2019
rustup for retag rename

This is the Miri side of rust-lang/rust#64503. Do not force-push!
@bors
Copy link
Contributor

bors commented Sep 18, 2019

⌛ Testing commit d610d9d with merge d83bcbd...

@bors
Copy link
Contributor

bors commented Sep 18, 2019

☀️ Test successful - checks-travis, status-appveyor
Approved by: RalfJung
Pushing d83bcbd to master...

@bors bors merged commit d610d9d into master Sep 18, 2019
@RalfJung RalfJung deleted the rustup-retag branch September 28, 2019 14:39
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants