[re-adding the lists, i hope you don't mind] On Wed, 10 May 2023 18:52:54 +0200 Thomas Koenig <tkoe...@netcologne.de> wrote:
> Hi Bernhard, > > both patches look good to me. Pushed as r14-664-g39f7c0963a9c00 and r14-665-gbdc10c2bfaceb3 Thanks! > > No user impact, so they should have the lowest possible impact :-) > > (And I didn't know about DEBUG_FUNCTION, that could come in handy > later). > > Thanks for the patch! > > Best regards > > Thomas
