Documentation: Describe git-gui Tools menu configuration options.

diff --git a/Documentation/cat-texi.perl b/Documentation/cat-texi.perl
index e3d8e9faa8c4b64c757080b89f304f78d30fbc17..dbc133cd3c1f19dd507014477e68b8ada78eab5e 100755 (executable)
--- a/Documentation/cat-texi.perl
+++ b/Documentation/cat-texi.perl
@@ -11,7 +11,7 @@
        if (s/^\@top (.*)/\@node $1,,,Top/) {
                push @menu, $1;
        }
-       s/\(\@pxref{\[URLS\]}\)//;
+       s/\(\@pxref{\[(URLS|REMOTES)\]}\)//;
        print TMP;
 }
 close TMP;