[release][build] Permission to merge
22 Nov
2017
22 Nov
'17
8: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
10:50 p.m.
On 22 Nov 2017 20:51, "Jürgen Hunold via Boost"
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.
2562
Age (days ago)
2562
Last active (days ago)
1 comments
2 participants
participants (2)
-
Daniel James -
Jürgen Hunold