Summary:
A bug in docusaurus makes relative URLs fail depending on how the page
was accessed, because the URL of a page in docs/ will end in / if
accessed directly or via hyperlink, but that / will be omitted when
clicking on the sidebar. The final / makes all the difference when
interpreting relative URLs so relative URLs are essentially broken.
See https://github.com/facebook/docusaurus/issues/2832 for more details.
This changes URL generation to generate URLs /docs/next/..., and
manually substitute relative URLs that had been written by hand.
Also fix a few other things about outdated links/comments.
Finally, `make doc-publish`.
Reviewed By: dulmarod
Differential Revision: D22117187
fbshipit-source-id: 32e2ba7e1
Summary:
Take all the issue type documentation in the website and add it to infer
itself so it can generate the website (see further diffs).
I mostly generated this diff by writing a script to call from `utop`
with various file lists to do most of the heavy lifting for me and make
sure I didn't forget any issue types: P132800781
Reviewed By: ngorogiannis
Differential Revision: D21934372
fbshipit-source-id: f3ea8c566
Jules Villard