Subject: Re: [boost] [release][build] Permission to merge
From: Daniel James (dnljms_at_[hidden])
Date: 2017-11-22 22:50:15
On 22 Nov 2017 20:51, "JÃ¼rgen Hunold via Boost" <boost_at_[hidden]>
> I'd like to merge commit e07c805e to master.
> This fixes
> with my PR from
Yes, and thanks for fixing this.