diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:11:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:11:50 +0100 |
| commit | 073b92396a68be30f77c80960a58ca562bb01f49 (patch) | |
| tree | d2ad366f28624196ebfe9c1eadf595dcb490fcdc /ide/ide_slave.ml | |
| parent | c047ecce6e4dba33df69a53a9e168999676c65db (diff) | |
| parent | ed18f926e4695acc730218925ca156abe56ba5fc (diff) | |
Merge PR #6753: [toplevel] Make toplevel state into a record.
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 6d1064d25..fe86df084 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -458,8 +458,9 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop _args doc = - set_doc doc; +let loop _args ~state = + let open Vernac.State in + set_doc state.doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in |