From 71b101172275a7c5872f6e8e70f9c0185f93f828 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 28 Jul 2015 12:30:14 +0200
Subject: Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)

File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.

There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
---
 lib/util.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'lib/util.mli')

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. *)
-- 
cgit v1.2.3