aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorpboutill2012-04-13 14:48:34 +0000
committerpboutill2012-04-13 14:48:34 +0000
commit29f7a2d6211a8b31cc39847be9d9d12a4dbbf449 (patch)
tree670bd9496a51475dc51c895eaf5a4b47076d2f26 /ide
parent1638f5df49ff81e174f6a1c6915a65c9b9d4adf5 (diff)
Browser documentation & CharSet under Windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/ideutils.ml5
-rw-r--r--ide/preferences.ml4
2 files changed, 5 insertions, 4 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index fd460c4e97..86045ee19a 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 dd4ba00b6f..11228f5da3 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";