Skip to content

Commit 0f5b6b3

Browse files
committed
Fix scripts/build_docs.sh
1 parent 5df7965 commit 0f5b6b3

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

scripts/build_docs.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ EOF
2424
# Fetch the docs cache if it exists
2525
mkdir -p website/docs
2626
mkdir -p docbuild/.lake/build/doc
27-
mv website/docs docbuild/.lake/build/doc
27+
mv website/docs/* docbuild/.lake/build/doc
2828

2929
# Initialise docbuild as a Lean project
3030
cd docbuild
@@ -38,7 +38,7 @@ MATHLIB_NO_CACHE_ON_UPDATE=1 # Disable an error message due to a non-blocking bu
3838
# Move them out of docbuild
3939
cd ../
4040
mkdir -p docs/build
41-
mv docbuild/.lake/build/doc docs/build
41+
mv docbuild/.lake/build/doc/* docs/build
4242

4343
# Clean up after ourselves
4444
rm -rf docbuild

0 commit comments

Comments
 (0)