aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index aa9938eb3..5093c9632 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -135,8 +135,8 @@ let (current:pref ref) =
(* text_font = Pango.Font.from_string "sans 12";*)
text_font = Pango.Font.from_string "Monospace 10";
- doc_url = "http://coq.inria.fr/doc/";
- library_url = "http://coq.inria.fr/library/";
+ doc_url = Coq_config.wwwrefman;
+ library_url = Coq_config.wwwstdlib;
show_toolbar = true;
contextual_menus_on_goal = true;