Revert previous change; there's a better way to do it.
diff --git a/Doc/tools/node2label.pl b/Doc/tools/node2label.pl
index eaf106f..a59d68e 100755
--- a/Doc/tools/node2label.pl
+++ b/Doc/tools/node2label.pl
@@ -41,7 +41,7 @@
if (defined($nodes{$node})) {
$label = $nodes{$node};
if (s/(HREF|href)=\"$node([\#\"])/$1=\"$label.html$2/g) {
- s/(HREF|href)=\"$label.html#l2h-\d+/$1=\"$label.html/g;
+ s/(HREF|href)=\"$label.html#(l2h-)?SECTION\d+/$1=\"$label.html/g;
$newnames{$node} = "$label.html";
}
}