aboutsummaryrefslogtreecommitdiff
path: root/lib/future.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-10-09 10:31:13 +0200
committerPierre-Marie Pédrot2015-10-09 10:31:13 +0200
commiteb7da0d0a02a406c196214ec9d08384385541788 (patch)
treeefe031d7df32573abd7b39afa0f009a6d61f18d5 /lib/future.mli
parent84add29c036735ceacde73ea98a9a5a454a5e3a0 (diff)
parent73daf37ccc7a44cd29c9b67405111756c75cb26a (diff)
Merge branch 'v8.5'
Diffstat (limited to 'lib/future.mli')
-rw-r--r--lib/future.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/future.mli b/lib/future.mli
index 324d5f7d10..de2282ae92 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
Thy are set for the outermos layer of the system, since they have to
deal with the whole system state. *)
val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
+val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit