diff options
Diffstat (limited to 'ide/minilib.mli')
| -rw-r--r-- | ide/minilib.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli index 22338250f4..1daa60e1a2 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -17,6 +17,8 @@ val list_filter_i : (int -> 'a -> bool) -> 'a list -> 'a list val list_chop : int -> 'a list -> 'a list * 'a list val list_index0 : 'a -> 'a list -> int +val string_map : (char -> char) -> string -> string + val subst_command_placeholder : string -> string -> string val home : string |