diff options
Diffstat (limited to 'runtime/doc/makehtml.awk')
| -rw-r--r-- | runtime/doc/makehtml.awk | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/runtime/doc/makehtml.awk b/runtime/doc/makehtml.awk index a1f77f5aba..216bb5fac1 100644 --- a/runtime/doc/makehtml.awk +++ b/runtime/doc/makehtml.awk @@ -185,12 +185,6 @@ FILENAME == "gui.txt" && asciiart == "no" \ asciicnt=0; } -FILENAME == "quotes.txt" && asciiart == "no" \ - && $0 ~ /In summary:/ { - asciiart= "yes"; - asciicnt=0; - } - FILENAME == "usr_20.txt" && asciiart == "no" \ && $0 ~ /an empty line at the end:/ { asciiart= "yes"; |