set_random_seed  2149 src/sysdep.c   static void set_random_seed (random_seed arg) { srandom (arg); }
set_random_seed  2152 src/sysdep.c   static void set_random_seed (random_seed arg) { srand48 (arg); }
set_random_seed  2155 src/sysdep.c   static void set_random_seed (random_seed arg) { srand (arg); }