Merge pull request #275 from korpling/feature/deploy-documentation

Add GitHub Action for deploying the developer guide on release

Author: thomaskrause

.github/workflows/deploy_documentation.yml

@@ -0,0 +1,33 @@
+on:
+    release:
+        types:
+            - published
+name: Deploy released binaries
+jobs:
+    deploy_documentation:
+        runs-on: ubuntu-latest
+        steps:
+            - name: Checkout
+              uses: actions/checkout@v1
+            - name: Get the release version from the GITHUB_REF variable as new SHORT_VERSION variable
+              run: echo "SHORT_VERSION=$(echo ${GITHUB_REF} | sed -E 's/^refs\/heads\/.*/develop/' | sed -E 's/^(refs\/tags\/v)?(.*)(\.[0-9]+\.[0-9]+)$/\2/')" >> $GITHUB_ENV
+            - run: misc/download-mdbook.sh 0.3.5
+              env:
+                  OS_NAME: linux
+            - name: Generate the documentation
+              run: mdbook build --dest-dir book/v${SHORT_VERSION} docs/
+            - run: git clone -q  -b gh-pages https://github.com/$GITHUB_REPOSITORY gh-pages
+            - name: Remove old files for this version
+              run: rm -Rf gh-pages/docs/v$SHORT_VERSION
+            - name: copy the documentation content
+              run: cp -R docs/book/* gh-pages/docs/
+            - run: git add docs/v$SHORT_VERSION
+              working-directory: gh-pages
+            - run: git -c user.name='gh-actions' -c user.email='gh-actions' commit --allow-empty -m "add documentation for version $SHORT_VERSION"
+              working-directory: gh-pages
+            - name: Push changes
+              uses: ad-m/github-push-action@v0.6.0
+              with:
+                  github_token: ${{ secrets.GITHUB_TOKEN }}
+                  directory: gh-pages
+                  branch: gh-pages