diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 444b2c2b..dba56a77 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 11058 2008-06-06 08:21:03Z herbelin $ *) +(* $Id: preferences.ml 11276 2008-07-28 00:28:34Z glondu $ *) open Configwin open Printf @@ -507,12 +507,11 @@ let configure ?(apply=(fun () -> ())) () = in let cmd_browse = let predefined = [ + Coq_config.browser; "netscape -remote \"openURL(%s)\""; "mozilla -remote \"openURL(%s)\""; - "firefox -remote \"openURL(%s,new-tab)\" || firefox %s &"; "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &"; "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"; - "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"; "open -a Safari %s &" ] in combo @@ -585,4 +584,3 @@ let configure ?(apply=(fun () -> ())) () = match x with | Return_apply | Return_ok -> save_pref () | Return_cancel -> () - |