Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
PR#7497: manual, numbered tables of contents #1095
Another point, as noticed by @dbuenzli, is that some warnings refer to the (relatively new) manual section 8.5 for a in-depth explanation. Unfortunately, without a numbered main table of contents, it is not trivial to find this section 8.5 in the manual.