diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index ee07b3fb81..f6ef42221c 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -106,7 +106,7 @@ object(self) then com ^ " " else com ^ " " ^ entry#text ^" . " in try - ignore(Coq.interp false phrase); + ignore(Coq.interp Coq.dummy_coqtop false phrase); result#buffer#set_text ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ()) with e -> |