Merge remote-tracking branch 'origin/master' into jahoti

1 files changed, 33 insertions, 0 deletions

diff --git a/process_html_file.sh b/process_html_file.sh
new file mode 100755
index 0000000..1ed0295
--- /dev/null
+++ b/process_html_file.sh
@@ -0,0 +1,33 @@
+#!/bin/sh
+
+# Copyright (C) 2021 Wojtek Kosior
+# Redistribution terms are gathered in the `copyright' file.
+
+# Call like:
+#     ./process_html_file.sh html/options.html
+
+. ./shell_utils.sh
+
+FILE="$1"
+FILEKEY=$(sanitize "$FILE")
+
+if [ "x$(map_get HTML_FILENAMES $FILEKEY)" = "xyes" ]; then
+    errcho "import loop on $FILE"
+    exit 1
+fi
+
+map_set_export HTML_FILENAMES $FILEKEY yes
+
+awk '\
+!/^[\t\r ]*<IMPORT[\t\r ]+([^\t\r ]+)[\t\r ]+\/>[\t\r ]*$/{
+	print $0;
+}
+/^[\t\r ]*<IMPORT[\t\r ]+([^\t\r ]+)[\t\r ]+\/>[\t\r ]*$/{
+    indent = substr($0, 1, index($0, "<") - 1);
+    command = "./process_html_file.sh " $2;
+    while (command | getline) {
+        print indent $0;
+    }
+    if (close(command) != 0)
+        exit 1;
+}' < "$FILE"