help.github.com seems to have a bug where HEAD on a redirected page
returns 404. This causes tools/test-documentation to fail. Fix it by
skipping the redirects.
Signed-off-by: Anders Kaseorg <andersk@mit.edu>
The testing section is more appropriate, since it's fundamentally part
of our CI system.
While we're at it, fix the fact that we were linking to GitHub, not
ReadTheDocs, in the run-mypy output.
This quiets the last of the warnings that Sphinx was giving us about
documents not being in any toctree, now that we've explicitly told it
with `:orphan:` about the documents we intentionally don't link there.
This updates the developer documentation to recommend `git clone -c`
to set the git pull mode to be rebase by default in the repository
configuration.
The hope is that this will help minimize how often new contributors
end up accidentally messing up their PRs by using `git pull`.
Tweaked by tabbott to fix broken links and optimize the language.
Fixes: #7022.
This commit helps reduce clutter on the navigation sidebar.
Creates new directories and moves relevant files into them.
Modifies index.rst, symlinks, and image paths accordingly.
This commit also enables expandable/collapsible navigation items,
renames files in docs/development and docs/production,
modifies /tools/test-documentation so that it overrides a theme setting,
Also updates links to other docs, file paths in the codebase that point
to developer documents, and files that should be excluded from lint tests.
Note that this commit does not update direct links to
zulip.readthedocs.io in the codebase; those will be resolved in an
upcoming follow-up commit (it'll be easier to verify all the links
once this is merged and ReadTheDocs is updated).
Fixes#5265.
Mateusz Mandera
Anders Kaseorg
Vishnu Ks
Tim Abbott
Jack Zhang
Abhigyan Khaund
Puneeth Chaganti
cg-cnu
Shivam Gera
Greg Price
Harshit Bansal
Mohd Ali Rizwi
David Rosa Tamsen