Clearing out old PRs

Hi folks,

The cache of formatted, but merged PRs is slowing things down substantially again. This happens when it grows too large. I used to prune them immediately, now I try to leave them for “a while” but I don’t have a system for determing how long “a while” is.

I’m going to clear them out today, anyway.

                                        Be seeing you,
                                          norm

--
Norm Tovey-Walsh
Saxonica