On Thu, Dec 22, 2022 at 10:32:22PM +0600, Илья Шипицин wrote: > I attached a patch. It keeps current behaviour and is safe to apply. > > in order to make a difference, github token must be issued and set via > github ci settings. > > Ilya >
I just pushed it, thank you. -- William Lallemand
