From 0f8ee8d0d33fcee3f095da9b17b390e56e8e083e Mon Sep 17 00:00:00 2001 From: Andreas Jaeger Date: Mon, 24 Aug 2015 21:28:15 +0200 Subject: [PATCH] Fix Debian Install Guide index name Rename index-debian.html to index.html. Change-Id: I9886fbc2bf3f9d1ecbb67ae72a28be08a5f4c800 --- tools/build-install-guides-rst.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tools/build-install-guides-rst.sh b/tools/build-install-guides-rst.sh index 0e2a60e065..61c2227c1b 100755 --- a/tools/build-install-guides-rst.sh +++ b/tools/build-install-guides-rst.sh @@ -21,3 +21,7 @@ for tag in obs rdo ubuntu debian; do tools/build-rst.sh doc/install-guide \ $GLOSSARY --tag ${tag} --target "draft/install-guide-${tag}" done + +# Debian uses index-debian, rename it. +mv publish-docs/draft/install-guide-debian/index-debian.html \ + publish-docs/draft/install-guide-debian/index.html