Plug into release.sh

This commit is contained in:
Clément Fournier 2018-05-18 01:41:41 +02:00
parent b22467e32a
commit 3687f9308e
2 changed files with 9 additions and 2 deletions

View File

@ -64,10 +64,15 @@ mkdir pmd.github.io
rsync -a ../docs/pmd-doc-${RELEASE_VERSION}/ pmd-${RELEASE_VERSION}/
git add pmd-${RELEASE_VERSION}
git commit -q -m "Added pmd-${RELEASE_VERSION}"
git rm -qr latest
cp -a pmd-${RELEASE_VERSION} latest
git add latest
git commit -q -m "Copying pmd-${RELEASE_VERSION} to latest"
./sitemap_generator.sh
git add sitemap.xml
git commit -q -m "Generated sitemap.xml"
git push origin master
)

View File

@ -6,8 +6,10 @@
WEBSITE_PREFIX="https://pmd.github.io/"
DOC_PREFIX="pmd-${RELEASE_VERSION}/"
LATEST_PRIORITY=0.8
DATE=`date +%Y-%m-%d`
# Priority is relative to the website, can be chosen in {0.1, 0.2, ..., 1}
# Default priority is 0.5
LATEST_PRIORITY=0.8
# Start of the output writing
@ -50,5 +52,5 @@ ENTRY_END
done
echo "</urlset>" >> sitemap.xml
echo "</urlset>" >> sitemap.xml