From 6b09f69e4da3c1fd491dbc5b475195a95636f636 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 26 Dec 2017 18:47:43 +0100
Subject: [ide] [doc] Document tweak to Query call.

---
 dev/doc/changes.md      | 7 +++++++
 dev/doc/xml-protocol.md | 6 ++++++
 2 files changed, 13 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 01aa6b599b..f6fbb69424 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -68,6 +68,13 @@ Declaration of printers for arguments used only in vernac command
   happen. An alternative is to register the corresponding argument as
   a value, using "Geninterp.register_val0 wit None".
 
+### XML IDE Protocol
+
+- Before 8.8, `Query` only executed the first command present in the
+ `query` string; starting with 8.8, the caller may include several
+ statements. This is useful for instance for temporarily setting an
+ option and then executing a command.
+
 ## Changes between Coq 8.6 and Coq 8.7
 
 ### Ocaml
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 18f6288f6f..b35571e9ca 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`.
   <string>${message}</string>
 </value>
 ```
+
+Before 8.8, `Query` only executed the first command present in the
+`query` string; starting with 8.8, the caller may include several
+statements. This is useful for instance for temporarily setting an
+option and then executing a command.
+
 -------------------------------
 
 
-- 
cgit v1.2.3