diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:36 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:36 +0000 |
| commit | 943cb0b91cfb15e2bdc04c626035e8cba0e65c02 (patch) | |
| tree | d8507a663c5be0814f4aea64b783975a3ad387a2 /ide/ideutils.mli | |
| parent | b6bd780dfab9cced833d09037a9c66f242b37053 (diff) | |
lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutils
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index cc34a355a..56183c520 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -91,3 +91,5 @@ val io_read_all : Glib.Io.channel -> string val run_command : (string -> unit) -> (Unix.process_status -> unit) -> string -> unit + +val glib_utf8_pos_to_offset : string -> off:int -> int |