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 <