Allow overriding platform.txt using platform.local.txt

This helps advanced users that want to change options (e.g. to use a
different toolchain or enable warnings), without having to change
platform.txt (which could make git report changed files all the time).
This commit is contained in:
Matthijs Kooijman 2014-04-04 10:33:20 +02:00
parent b2500b3b85
commit a46e503a30
1 changed files with 14 additions and 0 deletions

View File

@ -110,6 +110,20 @@ public class TargetPlatform {
format(_("Error loading {0}"), platformsFile.getAbsolutePath()), e);
}
// Allow overriding values in platform.txt. This allows changing
// platform.txt (e.g. to use a system-wide toolchain), without
// having to modify platform.txt (which, when running from git,
// prevents files being marked as changed).
File localPlatformsFile = new File(folder, "platform.local.txt");
try {
if (localPlatformsFile.exists() && localPlatformsFile.canRead()) {
preferences.load(localPlatformsFile);
}
} catch (IOException e) {
throw new TargetPlatformException(
format(_("Error loading {0}"), localPlatformsFile.getAbsolutePath()), e);
}
File progFile = new File(folder, "programmers.txt");
try {
if (progFile.exists() && progFile.canRead()) {