Skip to content

Merge branch '751-node' into 'master' #316

Merge branch '751-node' into 'master'

Merge branch '751-node' into 'master' #316

Workflow file for this run

name: GitHub Pages
on: [push]
jobs:
document:
runs-on: ubuntu-20.04
container:
image: ghcr.io/ricosjp/allgebra/cuda11_7/clang13/oss:22.05.4 #FIXME doxygen+clang14 bug
steps:
- uses: actions/checkout@v2
with:
fetch-depth: 0
- name: Install doxygen and graphviz
run: |
apt update
apt install -y doxygen graphviz
- name: work around permission issue
run: git config --global --add safe.directory /__w/monolish/monolish
- name: Generate document for current commit
run: |
cmake --preset=cpu-none-none
cmake --build build/cpu-none-none --target document
mv build/cpu-none-none/html .
- uses: actions/checkout@v2
with:
ref: gh-pages
path: public
- name: Update master document
if: ${{ github.ref == 'refs/heads/master' }}
run: |
rm -rf public/master
mv html public/master
- name: Update tag document
if: ${{ startsWith(github.ref, 'refs/tags' ) }}
run: |
export tag_name=$(basename ${{ github.ref }})
rm -rf public/${tag_name}
mv html public/${tag_name}
- name: deploy_pages
uses: peaceiris/actions-gh-pages@v3
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ./public/
force_orphan: true