Unnamed repository; edit this file 'description' to name the repository.
Auto merge of #3512 - RalfJung:miri-script-build, r=RalfJung
make miri-script a workspace root This is needed to make miri-script build on stable (as is done by the `./miri` script) when the parent package uses unstable cargo features.
bors 2024-04-25
parent 605fabe · parent 5db4475 · commit a8033ff
0 files changed, 0 insertions, 0 deletions