Skip to content

Yet another reorg

Yet another reorg #1

Workflow file for this run

name: Extras
on:
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]
env:
CARGO_TERM_COLOR: always
RUST_LOG: info
jobs:
book:
runs-on: ubuntu-20.04
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
steps:
- uses: actions/checkout@v2
- name: Setup mdBook
uses: peaceiris/actions-mdbook@v2
with:
mdbook-version: '0.4.10'
- run: mdbook build
- name: Deploy
uses: peaceiris/actions-gh-pages@v3
if: ${{ github.ref == 'refs/heads/main' }}
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ./book
# deploy:
# if: github.ref == 'refs/heads/main'
# needs: doc
# # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
# permissions:
# pages: write # to deploy to Pages
# id-token: write # to verify the deployment originates from an appropriate source
# # Deploy to the github-pages environment
# environment:
# name: github-pages
# url: ${{ steps.deployment.outputs.page_url }}
# runs-on: ubuntu-latest
# steps:
# - uses: actions/checkout@v3
# with:
# fetch-depth: 0
# - uses: actions/download-artifact@v4
# with:
# name: doc
# path: ${{ github.workspace }}
# - name: Upload Pages artifact
# uses: actions/upload-pages-artifact@v3
# with:
# path: target/doc
# - name: Deploy to GitHub Pages
# id: deployment
# uses: actions/deploy-pages@v4
# if: github.event_name != 'pull_request'