strftime() using '-' to remove leading 0s functionality removed or broken?

[Ed Morton]

Someone posted an answer at https://stackoverflow.com/a/77884684/1745001 
that puts a `-` in front of `strftime()` format specifiers to remove 
leading `0`s so that, for example, we can print the month number by doing:

   awk 'BEGIN{print strftime("%-m")}'

and get `1` output instead of the `01` we'd get with

   awk 'BEGIN{print strftime("%m")}'

That's consistent with how GNU date (and apparently various other tools) 
works:

   $ date +'%-m'
   1
   $

   $ date +'%m'
   01
   $

and it's what that SO answer shows with gawk 4.2.1.

When I try to do the same with gawk 5.0.0 or later, though, then I get:

   $ awk 'BEGIN{print strftime("%-m")}'

   $

   $ awk 'BEGIN{print strftime("%m")}'
   01
   $

i.e. adding the `-` makes `strftime()` produce no output.

That functionality isn't documented in the manual best I can tell - is 
that functionality that was removed or is it breakage or something else?

    Ed.