diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /ide/preferences.ml | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 -> () - |