Tweak deploy process

This commit is contained in:
Griatch 2020-06-13 00:34:37 +02:00
parent a809800707
commit 2d1d3b2472

View file

@ -12,9 +12,12 @@ fi
git checkout gh-pages
mv build ..
cd ..
rm -Rf docs/*
cp -Rf build/html/* docs/
git add docs/*
rm -Rf build
git commit -a -m "Updated HTML docs"
echo "Skipping deployment"