chore: fix CI

leanprover · Jul 4, 2024 · ca9d920 · ca9d920
1 parent 1f51169
commit ca9d920
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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