diff options
| author | bors <bors@rust-lang.org> | 2020-06-14 06:42:40 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2020-06-14 06:42:40 +0000 |
| commit | 10326d804e42022dee3de11e7a55b94028450f53 (patch) | |
| tree | 90e1c70157e0487653911b38c90e368461a21f8d /src/test/rustdoc/codeblock-title.rs | |
| parent | d3d3a14f2f17ae71d3e691743aadd62254d6521d (diff) | |
| parent | 416b010f4087d055febe2d55919f74e261ca8cd6 (diff) | |
| download | rust-10326d804e42022dee3de11e7a55b94028450f53.tar.gz rust-10326d804e42022dee3de11e7a55b94028450f53.zip | |
Auto merge of #73232 - RalfJung:miri-no-default, r=Mark-Simulacrum
x.py: do not build Miri by default on stable/beta Fixes https://github.com/rust-lang/rust/issues/73117 Do I need to do anything to make sure Miri is still built by the tools CI builder? Are there other tools that should be off-by-default? Also, unfortunately the `DEFAULT` associated const has no doc comment, so I have no idea what it does, or why there are semmingly two places where the default build of tools is controlled.
Diffstat (limited to 'src/test/rustdoc/codeblock-title.rs')
0 files changed, 0 insertions, 0 deletions