build/bin/write-dockerfile.sh [debian]: Handle EXTRA_PATH, EXTRA_SYST…

…EM_PACKAGES
sagemath · May 2, 2022 · a0e037f · a0e037f
1 parent d650177
commit a0e037f
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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 <<EOF