From 2d76a1df4c70d3321b0629d67dd5c5f84ac89567 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Sep 2010 10:18:18 +0000
Subject: Addressing part 2 of bug report 2377 (removing intrusive warning when
 coqide doc link is the canonical link to last released version of reference
 manual instead of link to corresponding coqide version).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/preferences.ml | 7 ++++++-
 lib/flags.ml       | 3 +--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index a99424cf75..a6aaef2576 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -266,7 +266,12 @@ let load_pref () =
     set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
     set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
     set_hd "doc_url" (fun v ->
-      if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url then
+      if not (Flags.is_standard_doc_url v) &&
+        v <> use_default_doc_url &&
+	(* Extra hack to support links to last released doc version *)
+        v <> Coq_config.wwwcoq ^ "doc" &&
+	v <> Coq_config.wwwcoq ^ "doc/"
+      then
 	prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);
       np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
diff --git a/lib/flags.ml b/lib/flags.ml
index cb450a5dba..8ec4a23512 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,8 +112,7 @@ let browser_cmd_fmt =
 
 let is_standard_doc_url url =
   let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
-  let wwwprefix = "http://coq.inria.fr/" in
-  let n = String.length wwwprefix in
+  let n = String.length Coq_config.wwwcoq in
   let n' = String.length Coq_config.wwwrefman in
   url = Coq_config.localwwwrefman ||
   url = Coq_config.wwwrefman ||
-- 
cgit v1.2.3