|
|
@ -36,6 +36,18 @@ jobs: |
|
|
|
make html |
|
|
|
make html |
|
|
|
rm -r ../docs/* |
|
|
|
rm -r ../docs/* |
|
|
|
cp -r _build/html ../docs |
|
|
|
cp -r _build/html ../docs |
|
|
|
|
|
|
|
git config --local user.email "f.martini@campus.unimib.it" |
|
|
|
|
|
|
|
git config --local user.name "philipMartini" |
|
|
|
|
|
|
|
git add . |
|
|
|
|
|
|
|
git commit -m "Update documentation" -a || true |
|
|
|
|
|
|
|
# The above command will fail if no changes were present, so we ignore |
|
|
|
|
|
|
|
# that. |
|
|
|
|
|
|
|
- name: Push changes |
|
|
|
|
|
|
|
uses: ad-m/github-push-action@master |
|
|
|
|
|
|
|
with: |
|
|
|
|
|
|
|
branch: master |
|
|
|
|
|
|
|
github_token: ${{ secrets.PYCTBN_TOK }} |
|
|
|
|
|
|
|
# =============================== |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|