diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-19 16:35:20 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-19 16:35:20 +0000 |
commit | 6fb3dd95c31216a294accedf4529fe05dad19bf0 (patch) | |
tree | 921d91423c605d756b60ec18b9c0452635d71586 /lib/system.mli | |
parent | 67bae3dcedbfe1c7ab4377fc4623b337fe4277b6 (diff) |
Déplacement de fonctionnalités unix et browser de ide vers lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.mli')
-rw-r--r-- | lib/system.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/lib/system.mli b/lib/system.mli index 40bacdec0..1ecd4bcff 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -50,6 +50,14 @@ val extern_intern : val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a +(*s [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 + passed to [f] *) + +val run_command : (string -> string) -> (string -> unit) -> string -> + Unix.process_status * string + (*s Time stamps. *) type time |