diff options
| author | Ralf Jung <post@ralfj.de> | 2020-09-21 10:40:49 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-21 10:40:49 +0200 |
| commit | d337074d0992533c02e077c562fc3ea279bd165c (patch) | |
| tree | 457a69a9ae49200555af215ac57b36992b6187ff | |
| parent | e177757a046ea5d667495181b8f5968bae71cfb6 (diff) | |
| parent | fc4b21fb6bfd4d966b9d30ce14442dd8af1c08c9 (diff) | |
| download | rust-d337074d0992533c02e077c562fc3ea279bd165c.tar.gz rust-d337074d0992533c02e077c562fc3ea279bd165c.zip | |
Rollup merge of #77000 - RalfJung:miri, r=RalfJung
update Miri I'd like to get https://github.com/rust-lang/miri/pull/1556 out there to avoid some backwards-incompatible changes. r? @ghost Cc @rust-lang/miri
| m--------- | src/tools/miri | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/tools/miri b/src/tools/miri -Subproject 5a15c8a6dd62033f69688f9d1c6eacd67415853 +Subproject cbc7560ae2d44669ef6ba0f43014e10ce881180 |