Leo Famulari writes: > 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. Alternatively, email control@debbugs.gnu.org with "close 12345". I see it also takes a "version" parameter, e.g. "close 12345 aaabbbccc". https://debbugs.gnu.org/server-control.html Useful if you don't want to spam list subscribers with an empty message.