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 dd8896cba..ec759b67f 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -117,7 +117,7 @@ object(self) | Interface.Fail (l,str) -> result#buffer#insert ("Error while interpreting "^phrase^":\n"^str); Coq.return () - | Interface.Good res | Interface.Unsafe res -> + | Interface.Good res -> result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res); Coq.return ()) in |