6 Jun
2018
6 Jun
'18
3:50 a.m.
On 5 June 2018 at 18:51, Xavier Besseron via Boost-users < boost-users@lists.boost.org> wrote:
I hope this will help.
Maybe you should/could create a PR, then in the future (if and when it get's merged, you don't have to fiddle with the boost code either). Have a good day, degski -- *"If something cannot go on forever, it will stop" - Herbert Stein*