aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extract_env.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-25 14:39:29 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-21 15:51:49 +0100
commit829a8feb3d02da057d39b5029b422e8a45dd1608 (patch)
treed2caa3d95e3c5462125c54745ed56ba924664dd6 /plugins/extraction/extract_env.ml
parent6e3fc0992be7ddd841328028dec51d390fffb851 (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 'plugins/extraction/extract_env.ml')
0 files changed, 0 insertions, 0 deletions