diff options
Diffstat (limited to 'otherlibs/labltk/browser/useunix.mli')
| -rw-r--r-- | otherlibs/labltk/browser/useunix.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/otherlibs/labltk/browser/useunix.mli b/otherlibs/labltk/browser/useunix.mli index 52ac7c770..2850c0d2d 100644 --- a/otherlibs/labltk/browser/useunix.mli +++ b/otherlibs/labltk/browser/useunix.mli @@ -18,5 +18,6 @@ val get_files_in_directory : string -> string list val is_directory : string -> bool +val concat : string -> string -> string val get_directories_in_files : path:string -> string list -> string list val subshell : cmd:string -> string list |