85 lines
3.7 KiB
YAML
85 lines
3.7 KiB
YAML
name: github pages
|
|
|
|
on:
|
|
push:
|
|
branches:
|
|
- main # deploy main. If your branch is `master`, you'll have to replace that throughout this file.
|
|
pull_request: # This will publish a site preview on every pull request, and also run the build command to test if the site is broken.
|
|
|
|
jobs:
|
|
deploy:
|
|
runs-on: ubuntu-22.04
|
|
env:
|
|
PR_PATH: pull/${{github.event.number}}
|
|
steps:
|
|
- name: Comment on PR
|
|
uses: hasura/comment-progress@v2.2.0
|
|
if: github.ref != 'refs/heads/main'
|
|
with:
|
|
github-token: ${{ secrets.GITHUB_TOKEN }}
|
|
repository: ${{ github.repository }}
|
|
number: ${{ github.event.number }}
|
|
id: deploy-preview
|
|
message: "Starting deployment of preview ⏳..."
|
|
|
|
- name: Set domain
|
|
run: echo "DOMAIN=lip6.github.io" >> $GITHUB_ENV # TODO set your custom domain
|
|
# If you're using the default github pages url, use this instead:
|
|
# run: echo "DOMAIN=${{ github.actor }}.github.io" >> $GITHUB_ENV
|
|
|
|
- name: Checkout website repo
|
|
uses: actions/checkout@v2
|
|
with:
|
|
submodules: true # fetch the theme
|
|
# you need to set this as an environment env if your repo or any submodules (e.g the theme) is private:
|
|
# token: ${{ secrets.PRIVATE_REPO_TOKEN }}
|
|
|
|
- name: Set production base URL
|
|
run: echo "BASE_URL=https://${{ env.DOMAIN }}/${{ github.event.repository.name }}/" >> $GITHUB_ENV
|
|
|
|
- name: Setup PDM
|
|
uses: pdm-project/setup-pdm@v3
|
|
|
|
- name: Build website
|
|
run: |
|
|
sudo apt install -y graphviz doxygen doxygen-latex python3-docutils qtbase5-dev libqt5svg5-dev
|
|
pdm sync -d --no-self
|
|
pdm run meson setup --prefix=/home/runner/work/install -D docs=true -D only-docs=true -D docs-siteurl=$BASE_URL builddir
|
|
pdm run meson install -C builddir
|
|
|
|
- name: Deploy if this is the `main` branch
|
|
uses: peaceiris/actions-gh-pages@v3
|
|
if: github.ref == 'refs/heads/main'
|
|
with:
|
|
github_token: ${{ secrets.GITHUB_TOKEN }}
|
|
publish_dir: /home/runner/work/install/share/doc/html
|
|
cname: ${{ env.DOMAIN }} # TODO you need to set this if you're using a custom domain. Otherwise you can remove it.
|
|
|
|
- name: Set base URL for preview if PR
|
|
if: github.ref != 'refs/heads/main'
|
|
run: echo "BASE_URL=https://${{ env.DOMAIN }}/${{ github.event.repository.name }}/${{ env.PR_PATH}}/" >> $GITHUB_ENV
|
|
|
|
- name: Build PR preview website
|
|
if: github.ref != 'refs/heads/main'
|
|
run: |
|
|
pdm run meson setup -D docs=true -D docs-siteurl=$BASE_URL builddir
|
|
pdm run meson install -C builddir
|
|
|
|
- name: Deploy to PR preview
|
|
uses: peaceiris/actions-gh-pages@v3
|
|
if: github.ref != 'refs/heads/main'
|
|
with:
|
|
github_token: ${{ secrets.GITHUB_TOKEN }}
|
|
publish_dir: /home/runner/work/install/share/doc/html
|
|
destination_dir: ${{ env.PR_PATH }} # TODO you need to set this if you're using a custom domain. Otherwise you can remove it.
|
|
|
|
- name: Update comment
|
|
uses: hasura/comment-progress@v2.2.0
|
|
if: github.ref != 'refs/heads/main'
|
|
with:
|
|
github-token: ${{ secrets.GITHUB_TOKEN }}
|
|
repository: ${{ github.repository }}
|
|
number: ${{ github.event.number }}
|
|
id: deploy-preview
|
|
message: "A preview of ${{ github.event.after }} is uploaded and can be seen here:\n\n ✨ ${{ env.BASE_URL }} ✨\n\nChanges may take a few minutes to propagate. Since this is a preview of production, content with `draft: true` will not be rendered. The source is here: https://github.com/${{ github.repository }}/tree/gh-pages/${{ env.PR_PATH }}/"
|