2023-05-13 18:28:34 +00:00
|
|
|
all:
|
|
|
|
|
@echo "Please specify a build target."
|
|
|
|
|
|
|
|
|
|
docs:
|
2023-05-14 16:51:30 +00:00
|
|
|
-ls build/doc | \
|
|
|
|
|
grep -v -E 'Init|Lean|Mathlib' | \
|
|
|
|
|
xargs -I {} rm -r "build/doc/{}"
|
|
|
|
|
-./scripts/run_pdflatex.sh build > /dev/null
|
|
|
|
|
lake build Bookshelf:docs
|
|
|
|
|
|
|
|
|
|
docs!:
|
2023-05-13 18:28:34 +00:00
|
|
|
-rm -r build/doc
|
|
|
|
|
-./scripts/run_pdflatex.sh build > /dev/null
|
|
|
|
|
lake build Bookshelf:docs
|
