diff options
| author | Maxime Dénès | 2016-06-27 15:16:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 18:35:08 +0200 |
| commit | d4725f692a5f202ca4c5d6341b586b0e377f6973 (patch) | |
| tree | 9cd74c65a51ca06547e9117b4d4901ec18a9519b /tools | |
| parent | 403c12ac3e8a9c3719aacbfa113600abc74846b7 (diff) | |
| parent | a10e3e0252560992128f490dfcb3d76c4bbf317b (diff) | |
Merge remote-tracking branch 'github/pr/223' into feedback-locations
Was PR#223: Allow feedback messages to carry a location.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/fake_ide.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 221fb36d8d..8fcca535d1 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -38,7 +38,7 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = let rec loop () = let xml = Xml_parser.parse coqtop.xml_parser in match Xmlprotocol.is_message xml with - | Some (level, content) -> + | Some (level, _loc, content) -> logger level content; loop () | None -> |