diff options
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/lib/system.mli b/lib/system.mli index 0c4bbd2284..e3fd5978c3 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,9 +8,12 @@ val is_in_path : string list -> string -> bool val where_in_path : string list -> string -> string val make_suffix : string -> string -> string +val file_readable_p : string -> bool val glob : string -> string +val home : string + (*s Global load path. *) val add_path : string -> unit @@ -34,8 +37,11 @@ val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) (*s Time stamps. *) -type time_stamp +type time + +val process_time : unit -> float * float +val get_time : unit -> time +val time_difference : time -> time -> float (* in seconds *) +val fmt_time_difference : time -> time -> Pp.std_ppcmds -val get_time_stamp : unit -> time_stamp -val compare_time_stamps : time_stamp -> time_stamp -> int |