Am Thu, Jul 27, 2023 at 12:59:21PM +0200 schrieb Andreas Enge: > PS: While trying to push I noticed that there is a branch wip-texlive > from January 2022; I suppose this can be deleted now?
Done. The branch appears to have been merged around that time. Andreas
