random_seed      2219 src/sysdep.c   static void set_random_seed (random_seed arg) { srandom (arg); }
random_seed      2222 src/sysdep.c   static void set_random_seed (random_seed arg) { srand48 (arg); }
random_seed      2225 src/sysdep.c   static void set_random_seed (random_seed arg) { srand (arg); }
random_seed      2231 src/sysdep.c     random_seed arg = 0;
random_seed      2242 src/sysdep.c     random_seed v;