Instructions for developers has been moved to its own page on the github.io documentation (preview here).
Adds the docs/ to .gitignore, so that the main branch will no longer track docs. Instead, documentation can be pushed separately to the gh-pages branch. See developer instructions for more details.
Some links may be broken until all repos have been moved to the new organization account (they have been changed preemptively). I will double-check them once we have finished migrating.
github.io
documentation (preview here).docs/
to.gitignore
, so that the main branch will no longer track docs. Instead, documentation can be pushed separately to thegh-pages
branch. See developer instructions for more details.