aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 11:11:50 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 11:11:50 +0100
commit073b92396a68be30f77c80960a58ca562bb01f49 (patch)
treed2ad366f28624196ebfe9c1eadf595dcb490fcdc /ide/coq.mli
parentc047ecce6e4dba33df69a53a9e168999676c65db (diff)
parented18f926e4695acc730218925ca156abe56ba5fc (diff)
Merge PR #6753: [toplevel] Make toplevel state into a record.
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 463dd134a..8c4727b37 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -171,3 +171,6 @@ val check_connection : string list -> unit
val interrupter : (int -> unit) ref
val save_all : (unit -> unit) ref
+
+(* Flags to be used for ideslave *)
+val ideslave_coqtop_flags : string option ref