Doppelte DIRECTORY_SEPARATORS entfernen.

Weil ich als RegEx erfahrener schon oft danach gefragt worden bin, wie man am saubersten mehrfache Separatoren hintereinander entfernen kann, hier ein kleiner Schnippsel.

$ds = DIRECTORY_SEPARATOR;
$source = preg_replace( '~('.$ds.')\1+~', '$1', $file );