For the header only version, the global variable default_random no more exist => we need to replace all occurences of default_random by a call to the global function get_default_random().
As usual, no modification for the non header only version.
All non-ASCII files should be encoded in UTF-8. So far, the ZSH script
`Scripts/developer_scripts/detect_wrong_encoding` detects wrong encoding
in source/header files of include/, src/, and doc/.