| name: Contrib Deploy |
| on: |
| push: |
| branches: |
| - master |
| |
| concurrency: |
| cancel-in-progress: false |
| group: "gh-pages" |
| |
| permissions: |
| contents: read |
| |
| jobs: |
| deploy: |
| permissions: |
| contents: write # for Git to git push |
| runs-on: ubuntu-latest |
| steps: |
| - uses: actions/checkout@v4 |
| with: |
| fetch-depth: 0 |
| - name: Install mdbook |
| run: | |
| mkdir mdbook |
| curl -Lf https://github.com/rust-lang/mdBook/releases/download/v0.4.27/mdbook-v0.4.27-x86_64-unknown-linux-gnu.tar.gz | tar -xz --directory=./mdbook |
| echo `pwd`/mdbook >> $GITHUB_PATH |
| - name: Deploy docs |
| run: | |
| GENERATE_PY="$(pwd)/ci/generate.py" |
| |
| cd src/doc/contrib |
| mdbook build |
| |
| # Override previous ref to avoid keeping history. |
| git worktree add --orphan -B gh-pages gh-pages |
| git config user.name "Deploy from CI" |
| git config user.email "" |
| cd gh-pages |
| mv ../book contrib |
| git add contrib |
| |
| # Generate HTML for link redirections. |
| python3 "$GENERATE_PY" |
| git add *.html |
| # WARN: The CNAME file is for GitHub to redirect requests to the custom domain. |
| # Missing this may entail security hazard and domain takeover. |
| # See <https://docs.github.com/en/pages/configuring-a-custom-domain-for-your-github-pages-site/managing-a-custom-domain-for-your-github-pages-site#securing-your-custom-domain> |
| git add CNAME |
| |
| git commit -m "Deploy $GITHUB_SHA to gh-pages" |
| git push origin +gh-pages |