diff options
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index e0a742779..dd8896cba 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -111,10 +111,9 @@ object(self) if String.get com (String.length com - 1) = '.' then com ^ " " else com ^ " " ^ entry#text ^" . " in - let log level message = result#buffer#insert (message^"\n") - in + let log level message = result#buffer#insert (message^"\n") in let process = - Coq.bind (Coq.interp ~logger:log ~raw:true phrase) (function + Coq.bind (Coq.interp ~logger:log ~raw:true 0 phrase) (function | Interface.Fail (l,str) -> result#buffer#insert ("Error while interpreting "^phrase^":\n"^str); Coq.return () |