Actually removing deprecated modules

Stream: PR reviews

[Jeremy Tan]

#32765 removes 6-month-old deprecated modules. I remember there's a script to auto-remove deprecated declarations, but it doesn't extend to modules yet

[Johan Commelin]

Thanks! I've kicked this on the merge queue.

[Johan Commelin]

But I noticed that a bot posted a boatload of warnings about these removed files. We should teach the bot that it shouldn't warn about removing files with a deprecation data > 6 months old.

[Ruben Van de Velde]

Dunno if it's worth complicating the bot, it's just a warning that you're entitled to dismiss

[Johan Commelin]

With PRs like these it would be helpful. Because it would confirm that indeed all 58 files were deprecated > 6 months ago.