On Thu, May 11, 2017 at 11:06:22PM +0200, Danny Milosavljevic wrote: > Hi Kei, > > > Never mind my other email... I see that the reason these are already on > > master is because they were already pushed there. Feel free to close > > these! > > Hehe yeah. I wonder though: If I put "Fixes > " into the commit log, does that mean that > something (a cron job etc) actually marks the bug report as fixed? > How often does that happen? It doesn't happen :) You have to send mail to the debbugs ticket. For example <12345-done@debbugs.gnu.org>, where 12345 is the bug number.