Skip to content

Commit

Permalink
small change in README
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Apr 19, 2024
1 parent d11122f commit 0890ea1
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ Note: To get this repository, you will need to download Lean's mathematical libr

## Building the blueprint

To test the Blueprint locally, you can compile `print.tex` using XeLaTeX (i.e. `xelatex blueprint/src/print.tex`). If you have the Python package `invoke` you can also run `inv bp`.
To test the Blueprint locally, you can compile `print.tex` using XeLaTeX (i.e. `xelatex print.tex` in the folder `blueprint/src`). If you have the Python package `invoke` you can also run `inv bp`.
If you feel adventurous and want to build the web version of the blueprint locally, you need to install some packages by following the instructions [here](https://pypi.org/project/leanblueprint/). But if the pdf builds locally, you can just make a pull request and use the online blueprint.

## Making a pull request
Expand Down
4 changes: 2 additions & 2 deletions blueprint/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
*.paux
*.aux
*.log
*.toc
print
web
__pycache__
Expand All @@ -13,5 +14,4 @@ __pycache__
*.maf
*.mtc
*.mtc0
build
*.toc
build

0 comments on commit 0890ea1

Please sign in to comment.