From 8756c0929a4c3cf778675d1597cb12d525d9a43a Mon Sep 17 00:00:00 2001
From: Trevor Spiteri <tspiteri@ieee.org>
Date: Wed, 24 Mar 2021 10:05:44 +0100
Subject: [PATCH] use awk with no gnu extensions in doc index generation

---
 etc/gen-doc-index.sh | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/etc/gen-doc-index.sh b/etc/gen-doc-index.sh
index d4d0780..70529ec 100755
--- a/etc/gen-doc-index.sh
+++ b/etc/gen-doc-index.sh
@@ -6,12 +6,22 @@ cd public
 cp dev/*/index.html index.html
 
 function filter {
-    gawk "$1" < index.html > index.html.tmp
+    awk "$1" < index.html > index.html.tmp
     mv index.html.tmp index.html
 }
 
-filter '{if ($0 ~ /button>$/) {printf "%s", $0; next}; print}'
-filter '{print gensub(/('\''|")\.\.\//, "\\1dev/", "g")}'
+filter '{
+    if ($0 ~ /button>$/) {
+        printf "%s", $0
+        getline
+    }
+    print
+}'
+filter '{
+    gsub(/'\''\.\.\//, "'\''dev/")
+    gsub(/"\.\.\//, "\"dev/")
+    print
+}'
 filter '{
     gsub(/<\/nav>/, "\013")
     sub(/<div class="block[^\013]*\013/, "\013")
@@ -30,10 +40,11 @@ filter '{
 
     print
 }'
-
 filter '{
     if ($0 ~ /<\/h1>/) {
-        print gensub(/(.*<\/h1>).*/, "\\1", 1)
+        h = $0
+        sub(/<\/h1>.*/, "</h1>", h)
+        print h
         sub(/.*<\/h1>/, "")
         while ($0 !~ /<\/section>/) { getline }
         while (getline line<"../etc/index-contents.html") { print line }