aboutsummaryrefslogtreecommitdiff
path: root/lib/util.mli
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 /lib/util.mli
parentaff5a1aaeb9b50c60ff32b7d5336a44fd18428ee (diff)
parent0dac9618c695a345f82ee302b205217fff29be29 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'lib/util.mli')
-rw-r--r--lib/util.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli
index 4fce809c2c..1dc405fcbe 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+
+val open_utf8_file_in : string -> in_channel
+(** Open an utf-8 encoded file and skip the byte-order mark if any. *)