Skip to content

Merge branch 'main' into chores-update-rewards #56

Merge branch 'main' into chores-update-rewards

Merge branch 'main' into chores-update-rewards #56

Workflow file for this run

# 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