Yes, PR#2781 was what I meant.o01eg wrote: ↑Sun Mar 08, 2020 9:12 pmDo you mean https://github.com/freeorion/freeorion/pull/2781 ? Feel free to merge it after CI finished.
Sorry, didn't get back to FO stuff until now, but you've merged that PR already, looks ok as far as I can tell.