Trac #30802: build/bin/write-dockerfile.sh: Do not fail with "build/pkgs/SPKG/type: No such file or directory"

When switching between branches, there are sometimes directories left in
the tree. Other code has already been adjusted so that only warnings are
emitted; but `build/bin/write-dockerfile.sh` still exits with an error.
We fix this in this ticket.

URL: https://trac.sagemath.org/30802
Reported by: mkoeppe
Ticket author(s): Matthias Koeppe
Reviewer(s): Dima Pasechnik

Author: Release Manager

build/bin/write-dockerfile.sh

@@ -17,8 +17,8 @@ for PKG_SCRIPTS in build/pkgs/*; do
     if [ -d $PKG_SCRIPTS ]; then
         PKG_BASE=$(basename $PKG_SCRIPTS)
         SYSTEM_PACKAGES_FILE=$PKG_SCRIPTS/distros/$SYSTEM.txt
-        PKG_TYPE=$(cat $PKG_SCRIPTS/type)
-        if [ -f $SYSTEM_PACKAGES_FILE -a -f $PKG_SCRIPTS/spkg-configure.m4 ]; then
+        if [ -f $PKG_SCRIPTS/type -a -f $SYSTEM_PACKAGES_FILE -a -f $PKG_SCRIPTS/spkg-configure.m4 ]; then
+           PKG_TYPE=$(cat $PKG_SCRIPTS/type)
            PKG_SYSTEM_PACKAGES=$(echo $(${STRIP_COMMENTS} $SYSTEM_PACKAGES_FILE))
            if [ -n "PKG_SYSTEM_PACKAGES" ]; then
                case "$PKG_TYPE" in