aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-07-29 12:12:35 +0200
committerPierre-Marie Pédrot2015-07-29 12:12:35 +0200
commite76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (patch)
tree5bcdbed2dac27feeb27caf840e8cad24e7483a9a /ide
parentaff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff)
parent0dac9618c695a345f82ee302b205217fff29be29 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'ide')
-rw-r--r--ide/ideutils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 67e4bdb0c9..5892fb3d96 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -311,7 +311,7 @@ let read_buffer = Buffer.create maxread
I/O Exceptions are propagated. *)
let read_file name buf =
- let ic = open_in name in
+ let ic = Util.open_utf8_file_in name in
let len = ref 0 in
try
while len := input ic read_string 0 maxread; !len > 0 do