[PATCH] new function for real local date

As there is no function for getting a real local date for day names and month names, I wrote a function for that. Maybe an option for a new PHP version? <?php function localdate(string $format, int $timestamp, string $locale) { $oldlocale = setlocale(LC_TIME, 0); setlocale(LC_TIME, $locale); $date = ''; for ($i = 0; $i < strlen($format); $i++) { $char = substr($format, $i, 1); switch ($char) { case 'D': $date .= strftime('%a', $timestamp); break; case 'l': $date .= strftime('%A', $timestamp); break; case 'M': $date .= strftime('%b', $timestamp); break; case 'F': $date .= strftime('%B', $timestamp); break; default: $date .= date($char, $timestamp); break; } } setlocale(LC_TIME, $oldlocale); return $date; } ?> with kind regards, Ruud Bakker