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