equal
deleted
inserted
replaced
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"]; |