You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Auto merge of #73232 - RalfJung:miri-no-default, r=Mark-Simulacrum
x.py: do not build Miri by default on stable/beta
Fixes#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.
0 commit comments