diff options
1 files changed, 6 insertions, 2 deletions
| -rw-r--r-- | awk-edits/Heading-anchors.awk | 8 |
diff --git a/awk-edits/Heading-anchors.awk b/awk-edits/Heading-anchors.awk index e3846f9..10f4aa9 100644 --- a/awk-edits/Heading-anchors.awk +++ b/awk-edits/Heading-anchors.awk @@ -7,6 +7,10 @@ # hyperlink is required (except for h1). /[ \t]*<h[23456]/ { - match($0, /id="[^"]*"/); - $0 = $0 ORS "<a class=\"h-anchor\" href=\"#" substr($0, RSTART + 4, RLENGTH - 5) "\" aria-hidden=\"true\">§</a>"; + if (match($0, /<h2 id="contents"/) == 0) { + match($0, /<h./) + gap = "<div class=\"gap" ((substr($0, RSTART + 2, 1) == 2) ? "" : "-small") "\"></div>" ORS + } + match($0, /id="[^"]*"/) + $0 = gap $0 ORS "<a class=\"h-anchor\" href=\"#" substr($0, RSTART + 4, RLENGTH - 5) "\" aria-hidden=\"true\">§</a>" } |