From aafe0040d6b4a69b4a6093a3262473e675387664 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Mon, 27 Aug 2018 17:24:24 +0900
Subject: Fix wwwrefman and wwwstdlib

---
 configure.ml | 4 ++--
 1 file 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;
-- 
cgit v1.2.3