diff options
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 44a89edf9..08739d013 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -922,7 +922,7 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in @@ -935,7 +935,7 @@ let configure ?(apply=(fun () -> ())) () = doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); + "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo |