Skip to content

Format spaces

Format spaces #18

Workflow file for this run

name: mdbook deploy to github pages
on:
push:
branches:
- master
jobs:
Build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v3
- name: Download mdbook for Lean
shell: bash
run: |
curl -O --location https://github.com/leanprover/mdBook/releases/download/v0.4.15l2/mdbook-linux.tar.gz
tar xvf mdbook-linux.tar.gz
./mdbook-linux/mdbook --help
ldd ./mdbook-linux/mdbook
- name: Run mdbook build
shell: bash
run: |
./mdbook-linux/mdbook build
rm -rf ./out/.git
rm -rf ./out/.github
- name: Deploy 🚀
uses: JamesIves/[email protected]
with:
branch: gh-pages
folder: out