Skip to content

fix Miri flag passing#23

Merged
dhardy merged 1 commit intorust-random:masterfrom
RalfJung:miri
Apr 24, 2021
Merged

fix Miri flag passing#23
dhardy merged 1 commit intorust-random:masterfrom
RalfJung:miri

Conversation

@RalfJung
Copy link
Contributor

With rust-lang/miri#1769 having landed, the old way of passing flags to Miri will soon stop working. This updates the CI to the new way.

Copy link
Member

@dhardy dhardy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@dhardy dhardy merged commit 7cda1f8 into rust-random:master Apr 24, 2021
takumi-earth pushed a commit to earthlings-dev/rngs that referenced this pull request Jan 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants