ich glaube, das ist nur was für Spezialisten und alte Hasen, nichts was uns Anfänger wirklich interessieren muss...

Übrigens, da gabs offenbar wirklich einen dicken Bug in der letzten IDE 1.6.12:

https://github.com/arduino/Arduino/issues/5430

ich kann allerdings nicht herauslesen, ob es nur Linux- oder auch Windows-PCs betraf...