On 18 July 2018 at 16:01, Philippe Mouawad <[email protected]> wrote: > On Wednesday, July 18, 2018, sebb <[email protected]> wrote: > >> It looks like JMeter PMC don't have karma to close other people's PRs. >> [That's probably because git is only a mirror.] > > > can’t this be changed by the way ?
Sorry, no idea. Try asking Infra. > It would makes things easier for us. > > >> >> If the originator does not respond, try making a dummy commit with the >> appropriate 'this fixes #nnn' comment. > > > Thanks, will do > >> >> On 18 July 2018 at 15:41, pmouawad <[email protected]> wrote: >> > Github user pmouawad commented on the issue: >> > >> > https://github.com/apache/jmeter/pull/393 >> > >> > Hello, >> > What is the purpose of this Pr ? >> > It looks like it’s empty. >> > >> > Can you close it please ? >> > >> > Thank you >> > >> > >> > --- >> > > > -- > Cordialement. > Philippe Mouawad.
