serendipity_strftime() does not convert date to local charset

[F3lisCatus]

My blog is set to using ISO 8859-1 instead of UTF-8 for historical reasons. After updating to 2.5.0 and PHP 8.2 I noticed the month on top of my entries was being displayed as a UTF-8 string ("März" instead of "März"). After some fiddling around with the source code and a short discussion on the forums (https://board.s9y.org/viewtopic.php?t=26376) I ended up adding the following line to /include/functions.inc.php:

# diff functions.inc.php functions.inc.php.orig 
163d162
<     if (LANG_CHARSET != "UTF-8") $out = mb_convert_encoding($out, LANG_CHARSET, 'UTF-8');

..which seems to work fine for me.