diff options
Diffstat (limited to 'library/library.mli')
| -rw-r--r-- | library/library.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/library/library.mli b/library/library.mli index f3899250e..0eb47bd3a 100644 --- a/library/library.mli +++ b/library/library.mli @@ -32,3 +32,8 @@ val require_module : bool option -> string -> string option -> bool -> unit val save_module_to : string -> string -> unit +(*s Global load path *) +val get_load_path : unit -> string list +val add_path : string -> unit +val rec_add_path : string -> unit +val remove_path : string -> unit |