Skip to content

Replace std::random_shuffle with std::shuffle

Marco Clemencic requested to merge clemenci/replace-random-shuffle into master

std::random_shuffle was deprecated in C++14 and (in principle) removed in C++17

Note: requires a change in the reference files in Boole and Rec

Merge request reports