Merge pull request #285 from RaitoBezarius/aeneas-docs #5
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
name: Build Aeneas user docs and test them | |
on: [push, pull_request] | |
jobs: | |
test: | |
name: Test Aeneas user docs | |
runs-on: [self-hosted, linux, nix] | |
steps: | |
- uses: actions/checkout@v4 | |
- name: Build the book | |
run: nix build '.?dir=docs/user'#book | |
# TODO: test the Lean examples code via nix build '.?dir=docs/user'#test or something similar. |