diff options
| author | Hugo Herbelin | 2019-05-09 00:36:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:26 +0200 |
| commit | e55ba2f04578738ec72c4ca64daf23b9ea51ec06 (patch) | |
| tree | 2d083b9eedc4ba5751c2e414d1dfc5d6f1230d9d /toplevel/workerLoop.ml | |
| parent | dd15e030be5e55d3770d27fbbc2fe0f5384f0166 (diff) | |
An attempt to reorganize further coqtop initialization into semantic units.
Incidentally moving parsing of "-batch" to the coqtop binary.
Diffstat (limited to 'toplevel/workerLoop.ml')
| -rw-r--r-- | toplevel/workerLoop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 6d147ac308..1fcc106348 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -14,7 +14,7 @@ let rec parse = function | [] -> [] let worker_parse_extra ~opts extra_args = - opts, parse extra_args + Coqtop.Interactive, parse extra_args let worker_init init ~opts = Flags.quiet := true; |