diff options
| author | coqbot-app[bot] | 2021-01-27 14:29:48 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-27 14:29:48 +0000 |
| commit | 8d697d8a4fe7165b736736196b167c5dc4725583 (patch) | |
| tree | 254e8f190cb63b00f2b1f448b6c6844342bbfe2f /toplevel/workerLoop.ml | |
| parent | 0c185094d40d10dc43f1432ef708a329fae25751 (diff) | |
| parent | 4d6c244ca6003991d6a3932461c5b1034e32b8f4 (diff) | |
Merge PR #13418: [sysinit] new component
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'toplevel/workerLoop.ml')
| -rw-r--r-- | toplevel/workerLoop.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index 59e10b09a0..e72940d189 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -8,10 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -let worker_parse_extra ~opts extra_args = - (), extra_args +let worker_parse_extra extra_args = + let stm_opts, extra_args = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extra_args in + ((),stm_opts), extra_args -let worker_init init () ~opts = +let worker_init init ((),_) _injections ~opts = Flags.quiet := true; init (); Coqtop.init_toploop opts @@ -27,9 +28,9 @@ let start ~init ~loop name = let open Coqtop in let custom = { parse_extra = worker_parse_extra; - help = worker_specific_usage name; - opts = Coqargs.default; - init = worker_init init; - run = (fun () ~opts:_ _state (* why is state not used *) -> loop ()); + usage = worker_specific_usage name; + initial_args = Coqargs.default; + init_extra = worker_init init; + run = (fun ((),_) ~opts:_ _state (* why is state not used *) -> loop ()); } in start_coq custom |