diff options
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/system.mli b/lib/system.mli index 13265d1d83..b887f5eb51 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,6 +1,13 @@ (* $Id$ *) +(*s Files and load path. *) + +val add_path : string -> unit +val del_path : string -> unit + +val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) + (*s Time stamps. *) type time_stamp |