"device/include/Makefile" ) CONFIG_FILES="$CONFIG_FILES device/include/Makefile" ;;
"support/librarian/Makefile" ) CONFIG_FILES="$CONFIG_FILES support/librarian/Makefile" ;;
"support/makebin/Makefile" ) CONFIG_FILES="$CONFIG_FILES support/makebin/Makefile" ;;
"device/include/Makefile" ) CONFIG_FILES="$CONFIG_FILES device/include/Makefile" ;;
"support/librarian/Makefile" ) CONFIG_FILES="$CONFIG_FILES support/librarian/Makefile" ;;
"support/makebin/Makefile" ) CONFIG_FILES="$CONFIG_FILES support/makebin/Makefile" ;;