Skip to content
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

Use Random.default_rng() instead of Random.GLOBAL_RNG #496

Closed
zsunberg opened this issue May 24, 2023 · 1 comment
Closed

Use Random.default_rng() instead of Random.GLOBAL_RNG #496

zsunberg opened this issue May 24, 2023 · 1 comment
Labels
Contribution Opportunity This would be something that would be very useful to the community and a good modular addition. Learning Opportunity Fixing this would be a good straightforward exercise to improve your julia coding skills. quick This task shouldn't take too long

Comments

@zsunberg
Copy link
Member

I think in POMDPs and POMDPTools we use GLOBAL_RNG quite a bit as a default - if I understand the intention of default_rng(), we should use that instead.

@zsunberg zsunberg added Contribution Opportunity This would be something that would be very useful to the community and a good modular addition. Learning Opportunity Fixing this would be a good straightforward exercise to improve your julia coding skills. quick This task shouldn't take too long labels May 24, 2023
@zsunberg
Copy link
Member Author

This was fixed by @NeroBlackstone in #503

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Contribution Opportunity This would be something that would be very useful to the community and a good modular addition. Learning Opportunity Fixing this would be a good straightforward exercise to improve your julia coding skills. quick This task shouldn't take too long
Projects
None yet
Development

No branches or pull requests

1 participant