Introduce command line options `--norepl` and `--nointeract`, remove `IsLIBGAP` constant#2723

Merged

markuspf merged 2 commits intogap-system:masterfrom markuspf:switch-off-repl

Aug 24, 2018

+15-24

Commits on Aug 24, 2018

Introduce command line options --norepl and --nointeract to disable GAP shell
Markus Pfeiffer
committed
Remove IsLIBGAP constant
Markus Pfeiffer
committed