Subject: [boost] [release][build] Permission to merge
From: Jürgen Hunold (jhunold_at_[hidden])
Date: 2017-11-22 20:50:43
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
Yours,
Jürgen
-- * Dipl.-Math. Jürgen Hunold ! * voice: ++49 4257 300 ! Fährstraße 1 * fax : ++49 4257 300 ! 31609 Balge/Sebbenhausen * jhunold_at_gmx.eu ! Germany