I wondered about that myself. Why bother building the docs? Isn’t that only needed for packaging/deployment? It ends up making PRs ugly because you have all the unnecessary docs in the diff.
-Jordan > On Nov 30, 2016, at 11:23 PM, Benjamin Reed <[email protected]> wrote: > > 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
