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 /stm | |
| 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 'stm')
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 6 |
2 files changed, 6 insertions, 1 deletions
diff --git a/stm/stm.mllib b/stm/stm.mllib index 4b254e811..72b538016 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,6 +5,7 @@ TQueue WorkerPool Vernac_classifier CoqworkmgrApi +WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 56fcf8537..50b42512c 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,9 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let rec parse args = args +let rec parse = function + | "--xml_format=Ppcmds" :: rest -> parse rest + | x :: rest -> x :: parse rest + | [] -> [] let loop init args = + let args = parse args in Flags.make_silent true; init (); CoqworkmgrApi.init !Flags.async_proofs_worker_priority; |