aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-30 09:39:54 +0200
committerMaxime Dénès2017-05-30 09:39:54 +0200
commitfd36c0451c26e44b1b7e93299d3367ad2d35fee3 (patch)
tree8b4d532931920ebf41941b2170282c63dd549c43 /ide/ideutils.ml
parentba3ccf80a44f0e06ee6e622a30f99de6804d005e (diff)
parenta0cec18b3ac2427aaf15d2808cf021a8931a2516 (diff)
Merge PR#356: Making management of installation directories more structured, more uniform
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a08ab07b5f..8a0e507c0b 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -422,7 +422,7 @@ let browse prerr url =
let doc_url () =
if doc_url#get = use_default_doc_url || doc_url#get = ""
then
- let addr = List.fold_left Filename.concat (Coq_config.docdir)
+ let addr = List.fold_left Filename.concat (Envars.docdir ())
["html";"refman";"index.html"]
in
if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman