diff options
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; |