From 861f892505f561f4e84436cfcfebb0642a4657ca Mon Sep 17 00:00:00 2001 From: t-bltg Date: Sun, 13 Oct 2024 21:06:15 +0200 Subject: [PATCH] Update ci_build.sh --- docs/ci_build.sh | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/docs/ci_build.sh b/docs/ci_build.sh index dd83e2d0f..d12fa6002 100644 --- a/docs/ci_build.sh +++ b/docs/ci_build.sh @@ -76,16 +76,22 @@ $julia -e ' ' echo "== build documentation for $GITHUB_REPOSITORY@$GITHUB_REF, triggered by $GITHUB_ACTOR on $GITHUB_EVENT_NAME ==" -$julia <