From 85237f65161cb9cd10119197c65c84f65f0262ee Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 18 Jan 2009 20:56:21 +0000 Subject: Backporting from v8.2 to trunk: - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/system.mli | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index 48e02cb5d..7556ed9e4 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -22,7 +22,7 @@ val exclude_search_in_dirname : string -> unit val all_subdirs : unix_path:string -> (physical_path * string list) list val is_in_path : load_path -> string -> bool -val where_in_path : bool -> load_path -> string -> physical_path * string +val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string val physical_path_of_string : string -> physical_path val string_of_physical_path : physical_path -> string @@ -36,7 +36,8 @@ val home : string val exists_dir : string -> bool -val find_file_in_path : load_path -> string -> physical_path * string +val find_file_in_path : + ?warn:bool -> load_path -> string -> physical_path * string (*s Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] @@ -50,8 +51,8 @@ exception Bad_magic_number of string val raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> in_channel) -val extern_intern : - int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) +val extern_intern : ?warn:bool -> int -> string -> + (string -> 'a -> unit) * (load_path -> string -> 'a) (*s Sending/receiving once with external executable *) -- cgit v1.2.3