diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 92dcd8222..beb8ebb52 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -104,9 +104,9 @@ object(self) then com ^ " " else com ^ " " ^ entry#text ^" . " in try - ignore(Coq.interp Coq.dummy_coqtop false phrase); + Coq.raw_interp Coq.dummy_coqtop phrase; result#buffer#set_text - ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ()) + ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop)) with e -> let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); |