Subject: Re: bug#21072: Brave new mark-defun (and a testing tool)

From: Marcin Borkowski <[email-masked]>
Date: Sun, 14 May 2017 07:13:22 +0200

On 2017-05-12, at 11:42, Marcin Borkowski <[email-masked]> wrote:

> All done, branch deleted and pushed again.  Hopefully it's ok now.  (I'm
> still learning to write commit messages...)

Hi all,

since seemingly nobody objected, I merged my branch into master and
marked the bug as done.

Best,

-- 
Marcin Borkowski