diff options
| author | bors <bors@rust-lang.org> | 2022-11-15 18:28:02 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2022-11-15 18:28:02 +0000 |
| commit | 209bcbb178fb1db833b628d4986c7ecc6ecb5884 (patch) | |
| tree | d2d951c9ea7f678de4769c30b28832ed7a1778ce /compiler/rustc_codegen_llvm/src | |
| parent | a046f62bb4230549dd5085e836705d6fe3ca86b3 (diff) | |
| parent | a47e4313901ac10071c8d41c43d9a3943b95e0ea (diff) | |
| download | rust-209bcbb178fb1db833b628d4986c7ecc6ecb5884.tar.gz rust-209bcbb178fb1db833b628d4986c7ecc6ecb5884.zip | |
Auto merge of #2667 - RalfJung:josh, r=RalfJung
adjust josh pushing, remove './miri toolchain HEAD/commit' Looks like pushing works much better if we use as base commit the last commit we pulled from rustc and merged into Miri. Which I guess is fair. Conveniently, the `rust-version` file should usually be pretty much exactly that commit. Also adjust `rustc-pull` to update that file. Pulling is now the way to update to a newer rustc, so I also removed `./miri toolchain HEAD`.
Diffstat (limited to 'compiler/rustc_codegen_llvm/src')
0 files changed, 0 insertions, 0 deletions