Revert previous change; there's a better way to do it.

diff --git a/Doc/tools/node2label.pl b/Doc/tools/node2label.pl
index eaf106fe88d14724676c10ca76715c97d4d7fad4..a59d68ed59916d2499f9081ef4779d1bf5294cdc 100755 (executable)
--- a/Doc/tools/node2label.pl
+++ b/Doc/tools/node2label.pl
@@ -41,7 +41,7 @@ while (<>) {
       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";
        }
       }