Re: [boost] [release][build] Permission to merge

On 22 Nov 2017 20:51, "Jürgen Hunold via Boost" wrote:

Hi!

I'd like to merge commit e07c805e to master.

This fixes

https://github.com/boostorg/build/issues/236

with my PR from

https://github.com/boostorg/build/pull/263

Yes, and thanks for fixing this.