+ local SBASE
+ if [ -n "$1" ] ; then
+ SDIR=`dirname "$1"`
+ local S=`basename "$1"`
+ SBASE=$(echo "$S" | sed 's/\.\([^.]\+\)//')
+ SRCEXT=$(echo "$S" | sed '/\./!d; s/.*\.\([^.]\+\)/\1/')
+ if [ -n "$SRCEXT" ] ; then
+ # Full name given, so just check the extension and existence
+ SRCN="$S"
+ [ -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