mirror of
https://github.com/esp8266/Arduino.git
synced 2025-06-17 22:23:10 +03:00
the same shell regardless of whether other shells are installed
(different shells have different behavior WRT directory component
separators, so this matters.
http://code.google.com/p/arduino/issues/detail?id=667 )
(cherry picked from commit fc8cacb9a3
)