yeah, that's a deeper question. pat or flavio can correct me on this, but i think the reason we check it in is so that the website's "trunk" documentation will work. now that we moved to git, i don't thing it works though... i also would just like to only build it when we do releases.
On Wed, Nov 30, 2016 at 2:24 PM, Jordan Zimmerman <[email protected]> wrote: > 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 >
