aboutsummaryrefslogtreecommitdiff
path: root/lib/serialize.mli
diff options
context:
space:
mode:
authorEnrico Tassi2013-11-25 10:13:32 +0100
committerEnrico Tassi2013-11-27 15:12:45 +0100
commitd5451ad4fc55c38ea0a7a1687dfc80c2bb0f9d13 (patch)
tree49eabbe2d581daff058760b86708395ad997e9e4 /lib/serialize.mli
parent217793d60211c88dbeb565a3fc62994a96a062ef (diff)
First stab at retrocompatible INTERP message
Diffstat (limited to 'lib/serialize.mli')
-rw-r--r--lib/serialize.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 2b1718bf76..e749462087 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -29,6 +29,8 @@ val get_options : get_options_sty -> get_options_rty call
val set_options : set_options_sty -> set_options_rty call
val quit : quit_sty -> quit_rty call
val init : init_sty -> init_rty call
+(* retrocompatibility *)
+val interp : interp_sty -> interp_rty call
val abstract_eval_call : handler -> 'a call -> 'a value