From ec5c0b41aed97d0109cfcf55837c18d473a07d91 Mon Sep 17 00:00:00 2001 From: Fred Drake Date: Wed, 10 Feb 1999 17:08:00 +0000 Subject: [PATCH] Revert previous change; there's a better way to do it. --- Doc/tools/node2label.pl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Doc/tools/node2label.pl b/Doc/tools/node2label.pl index eaf106fe88d..a59d68ed599 100755 --- 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"; } }