diff options
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index cb450a5db..8ec4a2351 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 || |