diff options
| author | Emilio Jesus Gallego Arias | 2018-08-28 13:06:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-28 13:06:38 +0200 |
| commit | a57891211e578605f6cb7e05f5fdadd7de49e519 (patch) | |
| tree | 6d0ff373cfd3ae87f226cef1909864647cb1dcab | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
| parent | aafe0040d6b4a69b4a6093a3262473e675387664 (diff) | |
Merge PR #8333: Fix URIs in the configuration script
| -rw-r--r-- | configure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/configure.ml b/configure.ml index 7fd900d995..7e0fd4c8ac 100644 --- a/configure.ml +++ b/configure.ml @@ -1214,8 +1214,8 @@ let write_configml f = pr_s "browser" browser; pr_s "wwwcoq" !prefs.coqwebsite; pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/"); - pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); - pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); + pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/refman/"); + pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "bytecode_compiler" !prefs.bytecodecompiler; pr_b "native_compiler" !prefs.nativecompiler; |