aboutsummaryrefslogtreecommitdiff
path: root/lib/options.mli
diff options
context:
space:
mode:
authorherbelin2005-05-19 16:35:20 +0000
committerherbelin2005-05-19 16:35:20 +0000
commit6fb3dd95c31216a294accedf4529fe05dad19bf0 (patch)
tree921d91423c605d756b60ec18b9c0452635d71586 /lib/options.mli
parent67bae3dcedbfe1c7ab4377fc4623b337fe4277b6 (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/options.mli')
-rw-r--r--lib/options.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/options.mli b/lib/options.mli
index 1c07799509..6b28158c3b 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -70,4 +70,9 @@ val print_bytecodes : unit -> bool
val set_boxed_definitions : bool -> unit
val boxed_definitions : unit -> bool
+(* Options for external tools *)
+
+(* Returns head and tail of printf string format *)
+(* ocaml doesn't allow not applied formats *)
+val browser_cmd_fmt : string * string