Introduce command line options --norepl and --nointeract, remove IsLIBGAP constant#2723
Merged
Merged
Commits
Commits on Aug 24, 2018
- committed
Markus Pfeiffer - committed
Markus Pfeiffer
--norepl and --nointeract, remove IsLIBGAP constant#2723