diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 14:48:34 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 14:48:34 +0000 |
commit | 29f7a2d6211a8b31cc39847be9d9d12a4dbbf449 (patch) | |
tree | 670bd9496a51475dc51c895eaf5a4b47076d2f26 | |
parent | 1638f5df49ff81e174f6a1c6915a65c9b9d4adf5 (diff) |
Browser documentation & CharSet under Windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | configure | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 5 | ||||
-rw-r--r-- | ide/preferences.ml | 4 |
3 files changed, 6 insertions, 5 deletions
@@ -388,7 +388,7 @@ fi if [ "$browser_spec" = "no" ]; then case $ARCH in - win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;; + win32) BROWSER='start %s' ;; Darwin) BROWSER='open %s' ;; *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;; esac diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fd460c4e9..86045ee19 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -279,11 +279,12 @@ let run_command f c = let browse f url = let com = Minilib.subst_command_placeholder !current.cmd_browse url in - let s = Sys.command com in + let _ = Unix.open_process_out com in () +(* This beautiful message will wait for twt ... if s = 127 then f ("Could not execute\n\""^com^ "\"\ncheck your preferences for setting a valid browser command\n") - +*) let doc_url () = if !current.doc_url = use_default_doc_url || !current.doc_url = "" then let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in diff --git a/ide/preferences.ml b/ide/preferences.ml index dd4ba00b6..11228f5da 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -119,8 +119,8 @@ let (current:pref ref) = read_project = Ignore_args; project_file_name = "_CoqProject"; - encoding_use_locale = true; - encoding_use_utf8 = false; + encoding_use_locale = Sys.os_type <> "Win32" ; + encoding_use_utf8 = Sys.os_type = "Win32" ; encoding_manual = "ISO_8859-1"; automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; |