fix: pipeline for new build

main
Henrik Böving 2022-08-11 23:49:30 +02:00
parent d43b23ec9f
commit de1405afd3
2 changed files with 1 additions and 9 deletions

View File

@ -25,14 +25,6 @@ jobs:
run: | run: |
lake build lake build
- name: Checkout and compile LeanInk
run: |
cd ../
git clone https://github.com/hargonix/LeanInk
cd LeanInk
git checkout doc-gen
lake build
- name: Checkout and compile mathlib4 - name: Checkout and compile mathlib4
run: | run: |
cd ../ cd ../

View File

@ -23,7 +23,7 @@ fi
# generate the docs # generate the docs
cd $1 cd $1
../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib lake -Kenv=dev build Mathlib:docs --verbose
if [ "$3" = "true" ]; then if [ "$3" = "true" ]; then
cd .. cd ..