Closed jzmaddock closed 10 years ago
What's with the duplicate pull requests?
Looks like John made separate pull requests for the master and develop branches. It's generally better to merge into develop, and then merge that into master. That way, you also merge into master the merge commit. So one pull request into develop should do (assuming develop can be safely merged into master, which should be true).
Correct, I made one for master and one for develop - basically because I really don't want to have to go through this patching process again next release. However, I don't mind how you merge them as long as the patch goes into master ;-)
There can be only one project named boost/doc and we have that already under /doc/ Change to something unique. Fixes PDF doc build.