web: Fix link to git branches.

The link broke several months ago in commit a2c5e36 which converted
the manual to markdown.

diff --git a/web/download.in.html b/web/download.in.html
index dd0b9c7838a0dfa3ecc85e9c8c9c731e8662d02d..a09fd1c868f5c9aa1eabd9b004d00dc30754d256 100644 (file)
--- a/web/download.in.html
+++ b/web/download.in.html
@@ -19,7 +19,7 @@ provided at this point. There are several ways to download the source:
                check out any of the four integration branches maint,
                master, next, pu (see the
 
-               <a href="manual.html#git_branches">git_branches</a>
+               <a href="manual.html#Git.branches">Git branches</a>
 
                section of the manual). All previous releases
                correspond to tagged commits and may be checked out