b0dfb76871
Currently, this configuration doesn't seem to be used yet, but regardless we'll update the settings to use RTEMS defaults.