echo -n '*** Your GCC does not produce working '; \
echo 'binaries in THUMB mode.'; \
echo '*** Your board is configured for THUMB mode.'; \
echo -n '*** Your GCC does not produce working '; \
echo 'binaries in THUMB mode.'; \
echo '*** Your board is configured for THUMB mode.'; \