aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r--ide/wg_Command.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 0ae57ee74..7d8993aa8 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -107,7 +107,7 @@ object(self)
let process =
Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function
| Interface.Fail (_,l,str) ->
- result#buffer#insert str;
+ Ideutils.insert_xml result#buffer str;
notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
Coq.return ()
| Interface.Good res ->