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
 
                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
 
                section of the manual). All previous releases
                correspond to tagged commits and may be checked out