diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:20:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:31:30 +0100 |
| commit | 7e992fa784ee6fa48af8a2e461385c094985587d (patch) | |
| tree | 3109d0608339cb49f24b96ff282709d8c4dab1a7 /ide/preferences.ml | |
| parent | dd47fcfc08c43288a49797cc72829da3f9642094 (diff) | |
Coqide: fixing default local links for refman and stdlib.
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 b16d45b54..f0fd45d77 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -918,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in @@ -931,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () = doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo |