diff --git a/tools/configure.sh b/tools/configure.sh index 5365b283a0..a9c271004d 100755 --- a/tools/configure.sh +++ b/tools/configure.sh @@ -148,11 +148,14 @@ if [ ! -d ${configpath} ]; then configpath=${TOPDIR}/${boardconfig} if [ ! -d ${configpath} ]; then - echo "Directory for ${boardconfig} does not exist." - echo "" - echo "Run tools/configure.sh -L to list available configurations." - echo "$USAGE" - exit 3 + configpath=${boardconfig} + if [ ! -d ${configpath} ]; then + echo "Directory for ${boardconfig} does not exist." + echo "" + echo "Run tools/configure.sh -L to list available configurations." + echo "$USAGE" + exit 3 + fi fi fi @@ -163,9 +166,9 @@ if [ ! -r ${src_makedefs} ]; then src_makedefs=${TOPDIR}/boards/*/*/${boarddir}/scripts/Make.defs if [ ! -r ${src_makedefs} ]; then - src_makedefs=${TOPDIR}/${boardconfig}/Make.defs + src_makedefs=${configpath}/Make.defs if [ ! -r ${src_makedefs} ]; then - src_makedefs=${TOPDIR}/${boardconfig}/../../scripts/Make.defs + src_makedefs=${configpath}/../../scripts/Make.defs if [ ! -r ${src_makedefs} ]; then echo "File Make.defs could not be found"