[release][build] Permission to merge
22 Nov
2017
22 Nov
'17
9:50 p.m.
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@gmx.eu ! Germany
22 Nov
22 Nov
11:50 p.m.
On 22 Nov 2017 20:51, "Jürgen Hunold via Boost" <boost@lists.boost.org> wrote:
Hi!
I'd like to merge commit e07c805e to master.
This fixes
https://github.com/boostorg/build/issues/236
with my PR from
Yes, and thanks for fixing this.
2900
Age (days ago)
2900
Last active (days ago)
1 comments
2 participants
participants (2)
-
Daniel James -
Jürgen Hunold