diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:06:42 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 16:06:42 +0000 |
commit | ccba6c718af6a5a15f278fc9365b6ad27108e98f (patch) | |
tree | f0229aa4d08eb12db1fb1e76f227076c117d59bf /lib/system.mli | |
parent | 06456c76b7fa2f0c69380faf27a6ca403b1e6f3f (diff) |
Various minor improvements of comments in mli for ocamldoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.mli')
-rw-r--r-- | lib/system.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/lib/system.mli b/lib/system.mli index 09142f365..d8a4088d0 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,12 +6,14 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {6 Sect } *) -(** Files and load paths. Load path entries remember the original root +(** System utilities *) + +(** {6 Files and load paths} *) + +(** Load path entries remember the original root given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) - type physical_path = string type load_path = physical_path list @@ -38,7 +40,7 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> load_path -> string -> physical_path * string -(** {6 Sect } *) +(** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] when the check fails, with the full file name. *) @@ -58,7 +60,7 @@ val extern_intern : ?warn:bool -> int -> string -> val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a -(** {6 Sect } *) +(** {6 Executing commands } *) (** [run_command converter f com] launches command [com], and returns the contents of stdout and stderr that have been processed with [converter]; the processed contents of stdout and stderr is also |