aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/fake_ide.ml')
-rw-r--r--tools/fake_ide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 221fb36d8..8fcca535d 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 ->