From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 11:41:40 +0200
Subject: [ide] Add route_id parameter to query call.

This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.

This change is necessary in order to fix bug ####.
---
 API/API.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 69278e7c9f..b5928c023d 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2266,10 +2266,9 @@ sig
                    | VtQed of vernac_qed_type
                    | VtProofStep of proof_step
                    | VtProofMode of string
-                   | VtQuery of vernac_part_of_script * report_with
+                   | VtQuery of vernac_part_of_script * Feedback.route_id
                    | VtStm of vernac_control * vernac_part_of_script
                    | VtUnknown
-   and report_with = Stateid.t * Feedback.route_id
    and vernac_qed_type = Vernacexpr.vernac_qed_type =
                        | VtKeep
                          | VtKeepAsAxiom
-- 
cgit v1.2.3