diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-25 14:39:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:49 +0100 |
| commit | 829a8feb3d02da057d39b5029b422e8a45dd1608 (patch) | |
| tree | d2caa3d95e3c5462125c54745ed56ba924664dd6 /ide/ide.mllib | |
| parent | 6e3fc0992be7ddd841328028dec51d390fffb851 (diff) | |
[xml] Restore protocol compatibility with 8.6.
By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
Diffstat (limited to 'ide/ide.mllib')
| -rw-r--r-- | ide/ide.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide.mllib b/ide/ide.mllib index 12170c462..78b4c01e8 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -14,6 +14,7 @@ Xml_parser Xml_printer Serialize Richpp +Topfmt Xmlprotocol Ideutils Coq |