aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/tacworkertop.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-01-31 05:22:31 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-02-09 23:02:59 +0100
commit56ba2afe14a19bd0d396f89cab3ae720f2664be3 (patch)
tree73a5ad4a3ee89559b78522c3fbc4ad14d17e0beb /stm/tacworkertop.ml
parent1222bc9e677c14884dd7c0f475003f01eb5fb1b1 (diff)
[toplevel] Refactor command line argument handling.
We mostly separate command line argument parsing from interpretation, some (minor) imperative actions are still done at argument parsing time. This tidies up the code quite a bit and allows to better follow the complicated command line handling code. To this effect, we group the key actions to be performed by the toplevel into a new record type. There is still room to improve.
Diffstat (limited to 'stm/tacworkertop.ml')
-rw-r--r--stm/tacworkertop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 17f90b7b1..f202fc7c5 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := (fun _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())