Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of #930 - RalfJung:build, r=RalfJung
test that build scripts do not run in Miri @elichai reported something that sounded a lot like build script running in Miri. But as this test shows, build scripts are not run by Miri, they are run normally. @elichai are you sure the [env var usage you were referring to](#641 (comment)) was only in a build script? Those shouldn't be affected by Miri flags at all. Is your code available somewhere so that I can try to reproduce?
- Loading branch information