+ if [ -n "$1" ] ; then
+ SRCBASE=$(echo $1 | sed 's/\.\([^.]\+\)//')
+ SRCEXT=$(echo $1 | sed 's/.*\.\([^.]\+\)/\1/')
+ if [ -n "$SRCEXT" ] ; then
+ # Full name given, so just check the extension and existence
+ SRCN=$1
+ if [ ${SRCN:0:1} == / ] ; then
+ SRCN=${SRCN:1}
+ SDIR=
+ fi
+ [ -f "$SDIR/$SRCN" ] || die "Cannot find source file $SDIR/$SRCN"
+ SRCEXT_OK=
+ for a in $EXTENSIONS ; do
+ if [ $a == $SRCEXT ] ; then
+ pend $SDIR/$SRCN
+ echo "Explicitly set source file: $SDIR/$SRCN"
+ return 0
+ fi
+ done
+ die "Unknown extension .$SRCEXT"
+ fi
+ else
+ SBASE=$PROBLEM
+ fi