From 5517623e8f9a1a5cb813a7d46aedb7ed22fb08c6 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Thu, 27 Feb 2025 14:51:04 +0100 Subject: [PATCH] Update build_docs.sh --- scripts/build_docs.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/build_docs.sh b/scripts/build_docs.sh index d00c2056..de8009a2 100755 --- a/scripts/build_docs.sh +++ b/scripts/build_docs.sh @@ -40,6 +40,7 @@ cd docbuild # Disable an error message due to a non-blocking bug. See Zulip MATHLIB_NO_CACHE_ON_UPDATE=1 ~/.elan/bin/lake update FLT +~/.elan/bin/lake exe cache get # Build the docs ~/.elan/bin/lake build FLT:docs