Merge branch 'master' into develop

This commit is contained in:
Griatch 2020-06-13 12:35:15 +02:00
commit 658b400afa

View file

@ -28,7 +28,7 @@ git add .
git commit -a -m "Updated HTML docs"
echo "Skipping deployment"
# git push origin gh-pages
git push origin gh-pages
# get back to previous branch
git checkout -