> On Nov 23, 2015, at 12:32 AM, Tomaz Muraus <[email protected]> wrote: > > I'm +1 for that (closing anything which is older than 6 months and / or not > relevant anymore). > > But yeah, what Jerry has said - we don't really have control over Github > PRs - we can only close them using references in the commit message. > > One thing we could do to close them is to push a dummy commit which > references all the PRs which are to be closed. >
Yes that’s the way to do it, we should come up with a list of all this PR. Ideally we can agree on this list what the PRs should be. Then push a dummy commit with ‘closes #XYZ" > On Mon, Nov 23, 2015 at 12:07 AM, anthony shaw <[email protected]> > wrote: > >> Hi, >> >> I'd like to cleanup any stale PRs in the current GitHub project, we still >> have open one's running all the way back to 2013. >> >> I think this is largely a case that people have forgotten about them, >> especially ones left with failing cases. >> >> I'm proposing we give a notice to any older than 2014 saying this will be >> closed in 30 days unless you respond. >> >> Any objections? >> >> Anthony >>
