mirror of
https://github.com/arduino/Arduino.git
synced 2025-04-03 20:25:18 +02:00
If two vendors declare the same tool (name and version) and platform.txt requires {runtime.tool-version.path}, the tool is chosen randomly. This patch completes 6f24fa6cec