Request to merge a fix to Boost.Core

From: Peter Dimov (pdimov_at_[hidden])
Date: 2023-07-26 07:13:05

May I please merge the following fix

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

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.