The commit message doesn't include "this closes " so nothing was triggered to close. Once this moves to gitbox we should be good.
John On Mon, Jun 4, 2018, 8:07 AM Jean-Louis MONTEIRO <[email protected]> wrote: > Hi, > > I have applied the PR/2 from Daniel Soro to SVN, but I can't close it. > Usually when Github is the mirror and we merge a PR manually, gitbot sees > it and closes the PR for us. > > Did I miss something? > > Jean-Louis >
