Pfadangaben in der php.ini, Strichpunkt und Doppelpunkt

Manchmal sucht man Fehler, die eigentlich gar keine sind - deshalb ist der entscheidende Hinweis aus der PHP-Dokumentation auch nochmal hier dupliziert:

Das Format ist ähnlich zur PATH-Umgebungsvariablen des jeweiligen Systems: Eine Liste von Verzeichnissen, getrennt durch einen Doppelpunkt unter Unix oder ein Semikolon unter Windows.

Nein, einfach kopieren zwischen verschiedenen Betriebssystemen geht nicht!