mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-30 19:52:13 +01:00
fc8cacb9a3
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 )