Skip to content

Commit

Permalink
chore: build PDFs on each change
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Jan 3, 2024
1 parent 8434d84 commit dd52495
Showing 1 changed file with 25 additions and 1 deletion.
26 changes: 25 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,31 @@ jobs:
run: |
lean --version
- name: build
- name: Build the project
run: |
lake build
- name: Install Dependencies
run: sudo apt update && sudo apt install -y pandoc texlive-latex-base texlive-latex-extra texlive-latex-recommended texlive-luatex fonts-dejavu


- name: Generate the manual
run: |
./generate.sh
cp _out/tex/main.pdf ./manual.pdf
- name: Upload PDF to artifact storage
if: github.ref != 'refs/heads/master'
uses: actions/upload-artifact@v3
with:
name: "LeanDoc manual"
path: "manual.pdf"

- uses: "marvinpinto/action-automatic-releases@latest"
if: github.ref == 'refs/heads/master'
with:
repo_token: "${{ secrets.GITHUB_TOKEN }}"
automatic_release_tag: "latest"
title: "LeanDoc manual"
files: |
manual.pdf

0 comments on commit dd52495

Please sign in to comment.