diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-18 11:35:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-19 11:43:41 +0200 |
| commit | d87bc5b9fb353655f8b905d73293abe96b0ad063 (patch) | |
| tree | a552df12fe9ab4bfd8575999b1945dea03e2c274 /ide/xmlprotocol.mli | |
| parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
Add XML protocol support for Wait.
Diffstat (limited to 'ide/xmlprotocol.mli')
| -rw-r--r-- | ide/xmlprotocol.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index d1c678b90..22117e35c 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -29,6 +29,8 @@ val set_options : set_options_sty -> set_options_rty call val quit : quit_sty -> quit_rty call val init : init_sty -> init_rty call val stop_worker : stop_worker_sty -> stop_worker_rty call +(* internal use (fake_ide) only, do not use *) +val wait : wait_sty -> wait_rty call (* retrocompatibility *) val interp : interp_sty -> interp_rty call val print_ast : print_ast_sty -> print_ast_rty call |