mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-30 19:52:13 +01:00
b816571772
That is, if the editor.languages.current preference is empty (or missing), use the default system locale.