when we commit pull requests with doc changes, i think we should commit the generated doc as a separate commit. what do you all think? i would like to do that to keep the change from the contributors pristine :) and i think it simplifies things a bit.
ben
