Add safety post-condition to unicode functions #39
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# This workflow is responsible for building and releasing the book. | |
name: Build Book | |
on: | |
workflow_dispatch: | |
pull_request: | |
branches: [ main ] | |
push: | |
paths: | |
- 'doc/**' | |
- '.github/workflows/book.yml' | |
jobs: | |
build: | |
runs-on: ubuntu-latest | |
steps: | |
- name: Checkout | |
uses: actions/checkout@v4 | |
- name: Install mdbook | |
run: | | |
cargo install mdbook --version "^0.4" --locked | |
echo "${HOME}/.cargo/bin" >> $GITHUB_PATH | |
# Removed --locked for now since it is broken due to old proc_macro feature. | |
- name: Install linkchecker | |
run: cargo install mdbook-linkcheck --version "^0.7" | |
- name: Build Documentation | |
run: mdbook build doc | |
- name: Upload book | |
uses: actions/upload-pages-artifact@v3 | |
with: | |
path: book/html | |
retention-days: "2" | |
deploy: | |
needs: build | |
runs-on: ubuntu-latest | |
if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} | |
# Grant GITHUB_TOKEN the permissions required to make a Pages deployment | |
permissions: | |
pages: write # to deploy to Pages | |
id-token: write # to verify source | |
environment: | |
name: github-pages | |
url: ${{ steps.deployment.outputs.page_url }} | |
steps: | |
- name: Deploy to GitHub Pages | |
id: deployment | |
uses: actions/deploy-pages@v4 |