Re: [boost] Request to merge a fix to Boost.Core

On Jul 26, 2023, at 12:13 AM, Peter Dimov via Boost wrote:

May I please merge the following fix

https://github.com/boostorg/core/commit/c7134904e27237dbbb81ba28f0f23fc365b0...

to address issue

https://github.com/boostorg/core/issues/150

?

I can't verify that the fix actually works, but it doesn't affect non-Android platforms, so can't make things any worse.

I see that Marcel has verified that it works. Go ahead. — Marshall