mirror of
https://github.com/arduino/Arduino.git
synced 2025-03-01 23:29:28 +01:00
This sorts the board submenus themselves, based on the displayed name. This does not change the ordering of board items within these submenus (which uses the order from boards.txt).