From a0e037f4df2f303423855351c4d5fc5001cca69f Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Mon, 2 May 2022 15:42:51 -0700 Subject: [PATCH] build/bin/write-dockerfile.sh [debian]: Handle EXTRA_PATH, EXTRA_SYSTEM_PACKAGES --- build/bin/write-dockerfile.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/build/bin/write-dockerfile.sh b/build/bin/write-dockerfile.sh index 4e2f891d506..e61d94b8e92 100755 --- a/build/bin/write-dockerfile.sh +++ b/build/bin/write-dockerfile.sh @@ -13,7 +13,7 @@ EXTRA_SAGE_PACKAGES="${5:-_bootstrap}" STRIP_COMMENTS="sed s/#.*//;" SAGE_ROOT=. export PATH="$SAGE_ROOT"/build/bin:$PATH -SYSTEM_PACKAGES= +SYSTEM_PACKAGES=$EXTRA_SYSTEM_PACKAGES CONFIGURE_ARGS="--enable-option-checking " for PKG_BASE in $($SAGE_ROOT/sage -package list --has-file=distros/$SYSTEM.txt $SAGE_PACKAGE_LIST_ARGS) $EXTRA_SAGE_PACKAGES; do PKG_SCRIPTS="$SAGE_ROOT"/build/pkgs/$PKG_BASE @@ -60,6 +60,9 @@ RUN $UPDATE $INSTALL software-properties-common && ($INSTALL gpg gpg-agent || ec RUN $SUDO add-apt-repository $EXTRA_REPOSITORY EOF fi + if [ -n "$EXTRA_PATH" ]; then + RUN="RUN export PATH=$EXTRA_PATH:\$PATH && " + fi ;; fedora*|redhat*|centos*) cat <