diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index d33c0add4..b83bd107e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -103,7 +103,7 @@ object(self) let process = Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer str; + Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str); notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> |