diff options
| author | Emilio Jesus Gallego Arias | 2017-04-19 23:24:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-20 00:15:12 +0200 |
| commit | 61b946cde62d3324c39f663974d4cfadd9207a69 (patch) | |
| tree | 3c87d311bc63ae3aadd878a51cf5813f820ef495 /plugins/syntax/string_syntax.ml | |
| parent | b3ed40b82540639de925afd36a32fbd716d2800f (diff) | |
[ide] Set Stateid in query pane.
We again remove another user of Stateid.dummy. However, we need to
adapt the protocol so `Coq.query` takes the `route_id` and we can
redirect the output properly to the subwindow.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions