Martin v. Löwis wrote:
Since I will probably add some documentation, and since this documentation will probably benefit from some reviews, what would be the best process ?
1/ commit the changeset and ask for a post-review by Georg (or others) 2/ hold the changeset in a diff for a pre-review ?
If you are confident that the documentation actually builds, feel free to commit it without pre-review. I recommend that you build the documentation at least once; I personally often commit documentation patches without testing first that they build when I'm confident about the markup I use.
1/ is better for the flow, but the quality of the doc might suffer from it if Georg (or others) doesn't have time to review it
This is of little concern. As long as the documentation continues to build (into html), nearly all documentation changes are improvements.
I agree with Martin here - breaking the documentation build isn't good, but other than that most doc changes are going to be OK.
And as for doing your own doc build, these days that should be as simple as changing to the Docs directory and typing "make html" (stale code in the Docs/tools directory can sometimes be a problem, but if you haven't built the docs before then that shouldn't come up).