Terminate make_device_config.sh if the awk command fails. Typically this means a missing file. Signed-off-by: Paul Brook <paul@codesourcery.com>
Allow default configs to be split into several files. Signed-off-by: Paul Brook <paul@codesourcery.com>