Publish docs

.github/workflows/documentation.yml

@@ -0,0 +1,52 @@
+name: Documentation
+permissions: read-all
+
+# Trigger for PR or merge to develop branch
+on:
+  push:
+    branches: develop
+    paths:
+      - 'docs/**'
+  pull_request:
+    paths:
+      - 'docs/**'
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@44c2b7a8a4ea60a981eaca3cf939b5f4305c123b # v4.1.5
+    - name: Configure & Build
+      run: |
+        cmake -DCMAKE_VERBOSE_MAKEFILE=on -B build docs
+        cmake --build build
+    - uses: actions/upload-artifact@v2
+      with:
+        name: docs
+        path: build/Documentation/html
+
+  publish:
+    needs: build
+    if: github.event_name == 'workflow_dispatch' || github.event_name == 'push' && github.ref == 'refs/heads/develop'
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@44c2b7a8a4ea60a981eaca3cf939b5f4305c123b # v4.1.5
+      with:
+        ref: gh-pages
+        path: gh-pages
+    - name: Remove old site
+      run: rm -rf gh-pages/*
+    - uses: actions/download-artifact@v2
+      with:
+        name: docs
+        path: gh-pages
+    - name: Push to GitHub Pages
+      run: |
+        cd gh-pages
+        touch .nojekyll
+        git add .
+        git config --global user.name "GitHub Actions"
+        git config --global user.email [email protected]
+        git commit -m "Update documentation"
+        git push --force origin gh-pages