diff options
| author | Emilio Jesus Gallego Arias | 2018-10-26 12:34:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-24 20:47:12 +0100 |
| commit | 8f9dcb8418ac4db5cf3e4302f61d543d0c47cbdf (patch) | |
| tree | 7c3722763bf495b56b6245640ab3d89b72f21a45 /ide | |
| parent | e0f55aecee2ed9fc6f56979c255688e08b136c20 (diff) | |
[toplevel] Allow to specify default options.
In some cases, toplevel ML clients may want to modify the default set
of flags that is passed to the main initalization routine. This is for
example useful for `idetop` to suppress some undesired printing at
startup.
I would say that clients ought to have more control, but I do expect
that PRs such as #8690 will help providing a better separation thus a
mode orthogonal API.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 8cb02190e6..a2b85041e8 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -537,5 +537,5 @@ let islave_init ~opts extra_args = let () = let open Coqtop in - let custom = { init = islave_init; run = loop; } in + let custom = { init = islave_init; run = loop; opts = Coqargs.default_opts } in start_coq custom |