Merge branch 'rr/push-head'

diff --git a/Documentation/cat-texi.perl b/Documentation/cat-texi.perl
index 828ec62554fe927eb16a03f835448e6db0c303a1..87437f8a95768595e040b8c4c1d48e5c29ada087 100755 (executable)
--- a/Documentation/cat-texi.perl
+++ b/Documentation/cat-texi.perl
@@ -12,6 +12,7 @@
                push @menu, $1;
        }
        s/\(\@pxref{\[(URLS|REMOTES)\]}\)//;
+       s/\@anchor\{[^{}]*\}//g;
        print TMP;
 }
 close TMP;