-
Notifications
You must be signed in to change notification settings - Fork 13.3k
minor improvements on running miri #140898
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
Signed-off-by: onur-ozkan <[email protected]>
Signed-off-by: onur-ozkan <[email protected]>
r? @clubby789 rustbot has assigned @clubby789. Use |
I assume Ralf uses this API a lot, it's worth pinging him to make sure he will be aware of this change (especially the second commit as the first one doesn't affect anything on the user side). cc @RalfJung |
I have no idea what the first commit does from a user perspective. The second commit looks good, except for the comment I added. :) |
Yes second commit also lgtm but I'm not sure of what the first is doing 😅 |
Sure. r? bootstrap |
It should be clear from the commit messages when reviewing them one by one.