Check-in by ben on 2025-01-19 20:43:07

 When formatting HTML content, replace tab escapes with eight
 spaces.  Prior to this commit, only tab characters were being
 replaced with eight spaces.

 INSERTED    DELETED
        1          0 src/web.awk
        1          0 TOTAL over 1 changed file

Index: src/web.awk
==================================================================
--- src/web.awk
+++ src/web.awk
@@ -127,10 +127,11 @@
    cmd = sprintf("%s -a -n 3 <%s | %s -ilr -w 60", cmd_strings, work, \
        cmd_webdump)
    marker = 999999
    while ((cmd | getline) > 0) {
        gsub(/\t/, "        ")
+        gsub(/\\t/, "        ")
        if (NR < marker) {
            if ($0 ~ /^References$/) {
                marker = NR
            }
            print

You are viewing proxied material from tilde.pink. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.