aboutsummaryrefslogtreecommitdiff
path: root/ide/command_windows.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/command_windows.ml')
-rw-r--r--ide/command_windows.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 9792d8782f..939238d3a3 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -102,7 +102,7 @@ object(self)
in
try
result#buffer#set_text
- (match Coq.interp coqtop ~raw:true phrase with
+ (match Coq.interp !coqtop ~raw:true phrase with
| Interface.Fail (l,str) ->
("Error while interpreting "^phrase^":\n"^str)
| Interface.Good results ->