diff options
Diffstat (limited to 'lib/options.ml')
| -rw-r--r-- | lib/options.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml index f190519f1f..45f27107e3 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -117,3 +117,10 @@ let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b let boxed_definitions _ = !boxed_definitions +(* Options for external tools *) + +let browser_cmd_fmt = + if Sys.os_type = "Win32" + then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" + else "netscape -remote \"OpenURL(", ")\"" + |