tools/lgf-gen.cc
changeset 618 b95898314e09
parent 612 0c8e5c688440
child 623 7c1324b35d89
equal deleted inserted replaced
4:9a2445cc8a2e 5:9bab1296175b
   718     .onlyOneGroup("rand")
   718     .onlyOneGroup("rand")
   719     .other("[prefix]","Prefix of the output files. Default is 'lgf-gen-out'")
   719     .other("[prefix]","Prefix of the output files. Default is 'lgf-gen-out'")
   720     .run();
   720     .run();
   721 
   721 
   722   if (ap["rand"]) {
   722   if (ap["rand"]) {
   723     int seed = time(0);
   723     int seed = int(time(0));
   724     std::cout << "Random number seed: " << seed << std::endl;
   724     std::cout << "Random number seed: " << seed << std::endl;
   725     rnd = Random(seed);
   725     rnd = Random(seed);
   726   }
   726   }
   727   if (ap.given("seed")) {
   727   if (ap.given("seed")) {
   728     int seed = ap["seed"];
   728     int seed = ap["seed"];