On Sun, Sep 03, 2023 at 02:07:19PM +0200, Florian Obser wrote: > Thanks, this is in know. > > How long should I leave the github repo in place? Do bulk builders care? > This is also not the most important package in the world...
You should be fine to remove it right after commit, pretty sure bulk builders do fetch distfiles before every build.
