18 Nov
2020
18 Nov
'20
5:52 p.m.
On Wed, Nov 18, 2020 at 9:38 AM Glen Fernandes via Boost
This is a PR to develop, which you don't need permission to merge.
What he's saying is that this change will also need to go into the master branch when the docca changes are merged to master. Thanks