diff options
| author | Emilio Jesus Gallego Arias | 2017-03-21 17:54:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-16 05:34:25 +0100 |
| commit | d941f739dd51f5702bccd8a61ed08027fb0fb264 (patch) | |
| tree | 198a4e7b31f0479431c067bf673c313ba88949ee /API/API.mli | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
[stm] [ide protocol] Allow to include several commands on query.
This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions