Archive web-rmtools?

Hi all! About a week ago I had opened an issue suggesting to archive web-rmtools[1], and since there have not been any objections, I'm asking here: Are there any objections against archiving web-rmtools? Note that I still don't think that this code has ever been used for anything else than Windows builds (and is no longer used for that purpose for a long time), since it is listed in the web- "namespace", I've cc'd the Webmaster mailing list. [1] <https://github.com/php/web-rmtools/issues/22> Cheers, Christoph