diff --git a/test_docs.sh b/test_docs.sh index bc3a73d7..b33bf33e 100755 --- a/test_docs.sh +++ b/test_docs.sh @@ -7,7 +7,7 @@ set -x # generate the docs cd "$1" -sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\"|" lakefile.lean +echo 'require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" from ".." / "doc-gen4"' >> lakefile.lean -lake -R -Kdoc=on update -lake -R -Kdoc=on build Batteries:docs +lake update doc-gen4 +lake build Batteries:docs