Hi Bruno, Bruno Haible <[email protected]> writes:
> Yes please. > >> Not sure if there was a reason for keeping them after moving to git. > > There was a CVS mirror of the git repository for a while, after we moved > to git. But by now, it's surely dead (or irrelevant) for a long time. Thanks. Removed them [1]. Collin [1] https://git.savannah.gnu.org/cgit/gnulib.git/commit/?id=ec28c077a704c29679f60d3e877688d5985e3452
