diff options
| author | Guillaume Melquiond | 2015-07-28 12:30:14 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-28 12:30:14 +0200 |
| commit | 71b101172275a7c5872f6e8e70f9c0185f93f828 (patch) | |
| tree | 3d31693af2a5f595b5a8f8cbab3438c3bb6cd18d /dev/include | |
| parent | 6d8d39fd0a1c7dac1b6415660fd97fe3ad010ff7 (diff) | |
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.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions