Request to merge a fix to Boost.Core

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.

On Jul 26, 2023, at 12:13 AM, Peter Dimov via Boost <boost@lists.boost.org> 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
participants (2)
-
Marshall Clow
-
Peter Dimov