web: Fix internal link to manual.
authorAndre Noll <maan@tuebingen.mpg.de>
Thu, 4 Nov 2021 20:14:57 +0000 (21:14 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Sat, 6 Nov 2021 19:11:51 +0000 (20:11 +0100)
This must have worked at some point...

Looks like it's no good idea to assume that these identifiers are
stable across markdown versions...

web/download.in.html

index 9ef92b7..b2b1f5f 100644 (file)
@@ -19,7 +19,7 @@ provided at this point. There are several ways to download the source:
                checkout of 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