index e3d8e9faa8c4b64c757080b89f304f78d30fbc17..dbc133cd3c1f19dd507014477e68b8ada78eab5e 100755 (executable)
if (s/^\@top (.*)/\@node $1,,,Top/) {
push @menu, $1;
}
- s/\(\@pxref{\[URLS\]}\)//;
+ s/\(\@pxref{\[(URLS|REMOTES)\]}\)//;
print TMP;
}
close TMP;