diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index ae6db1a7ac..9b7dcd67a1 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -27,8 +27,6 @@ let flash_info = let set_location = ref (function s -> failwith "not ready") -let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT - (** A utf8 char is either a single byte (ascii char, 0xxxxxxx) or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) |