From 7b3ec92f4807b05ed4e6472935dc0549125a1de0 Mon Sep 17 00:00:00 2001 From: Jesper Stemann Andersen Date: Thu, 14 Dec 2023 09:16:12 +0100 Subject: [PATCH] Init script: Added possiblity for overriding JULIAUP_VERSION --- deploy/shellscript/juliaup-init.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/deploy/shellscript/juliaup-init.sh b/deploy/shellscript/juliaup-init.sh index 0439be90..42eb5889 100644 --- a/deploy/shellscript/juliaup-init.sh +++ b/deploy/shellscript/juliaup-init.sh @@ -25,7 +25,9 @@ set -u # If JULIAUP_SERVER is unset or empty, default it. JULIAUP_SERVER="${JULIAUP_SERVER:-https://julialang-s3.julialang.org}" -JULIAUP_VERSION="THISISREPLACEDWITHREALVERSIONINGITHUBWORKFLOW" + +# If JULIAUP_VERSION is unset or empty, default it. +JULIAUP_VERSION="${JULIAUP_VERSION:-THISISREPLACEDWITHREALVERSIONINGITHUBWORKFLOW}" #XXX: If you change anything here, please make the same changes in setup_mode.rs usage() {