From 379b5b225eb28fb90b269349cf88e4f080ffddb9 Mon Sep 17 00:00:00 2001 From: t-bltg Date: Sun, 13 Oct 2024 20:46:58 +0200 Subject: [PATCH] Update ci_build.sh --- docs/ci_build.sh | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/docs/ci_build.sh b/docs/ci_build.sh index 4c5dbd245..dd83e2d0f 100644 --- a/docs/ci_build.sh +++ b/docs/ci_build.sh @@ -76,12 +76,16 @@ $julia -e ' ' echo "== build documentation for $GITHUB_REPOSITORY@$GITHUB_REF, triggered by $GITHUB_ACTOR on $GITHUB_EVENT_NAME ==" -$julia -e 'using Pkg; Pkg.develop([ +$julia <