1
0
mirror of https://github.com/arduino/Arduino.git synced 2025-01-19 08:52:15 +01:00

Pass runtime tools to arduino-builder

This commit is contained in:
Martino Facchin 2016-08-02 12:53:49 +02:00 committed by Cristian Maglie
parent fa0678f5b7
commit 6f24fa6cec
2 changed files with 8 additions and 0 deletions

View File

@ -51,6 +51,7 @@ import java.nio.file.StandardCopyOption;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Map;
import java.util.regex.Pattern;
import java.util.stream.Collectors;
import java.util.stream.Stream;
@ -235,6 +236,12 @@ public class Compiler implements MessageConsumer {
commandLine.addArgument("-prefs=build.warn_data_percentage=" + PreferencesData.get("build.warn_data_percentage"));
for (Map.Entry<String, String> entry : BaseNoGui.getBoardPreferences().entrySet()) {
if (entry.getKey().startsWith("runtime.tools")) {
commandLine.addArgument("-prefs=" + entry.getKey() + "=" + entry.getValue());
}
}
//commandLine.addArgument("-debug-level=10", false);
if (verbose) {

View File

@ -169,6 +169,7 @@ public class BaseNoGui {
for (ContributedTool tool : platform.getResolvedTools()) {
File folder = tool.getDownloadableContribution(getPlatform()).getInstalledFolder();
String toolPath = folder.getAbsolutePath();
prefs.put(prefix + tool.getName() + ".path", toolPath);
PreferencesData.set(prefix + tool.getName() + ".path", toolPath);
PreferencesData.set(prefix + tool.getName() + "-" + tool.getVersion() + ".path", toolPath);
}