Deploy GitHub pages using an Action instead of a special branch.

This commit is contained in:
Patrick Lehmann
2025-12-14 23:25:08 +01:00
parent 18379306db
commit e5a874819f
2 changed files with 25 additions and 19 deletions

View File

@@ -68,7 +68,7 @@ on:
jobs:
Extract:
name: 📓 Extract configurations from pyproject.toml
name: 🔬 Extract configurations from pyproject.toml
runs-on: "ubuntu-${{ inputs.ubuntu_image_version }}"
outputs:
unittest_report_xml: ${{ steps.getVariables.outputs.unittest_report_xml }}

View File

@@ -45,16 +45,24 @@ on:
default: ''
type: string
outputs:
github_pages_url:
description: "URL to GitHub Pages."
value: ${{ jobs.PrepareGitHubPages.outputs.github_pages_url }}
jobs:
PublishToGitHubPages:
name: 📚 Publish to GH-Pages
PrepareGitHubPages:
name: 📖 Merge multiple contents for publishing
runs-on: "ubuntu-${{ inputs.ubuntu_image_version }}"
permissions:
pages: write # to deploy to Pages
id-token: write # to verify the deployment originates from an appropriate source
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
outputs:
github_pages_url: ${{ steps.deployment.outputs.page_url }}
steps:
- name: ⏬ Checkout repository
uses: actions/checkout@v6
- name: 📥 Download artifacts '${{ inputs.doc }}' from 'SphinxDocumentation' job
uses: pyTooling/download-artifact@v7
with:
@@ -75,15 +83,13 @@ jobs:
name: ${{ inputs.typing }}
path: public/typing
- name: '📓 Publish site to GitHub Pages'
- name: 📑 Upload static files as artifact
if: github.event_name != 'pull_request'
run: |
cd public
touch .nojekyll
git init
cp ../.git/config ./.git/config
git add .
git config --local user.email "BuildTheDocs@GitHubActions"
git config --local user.name "GitHub Actions"
git commit -a -m "update ${{ github.sha }}"
git push -u origin +HEAD:gh-pages
uses: actions/upload-pages-artifact@v4
with:
path: public/
- name: 📖 Deploy to GitHub Pages
id: deployment
if: github.event_name != 'pull_request'
uses: actions/deploy-pages@v4