diff options
Diffstat (limited to 'runtime/doc/makehtml.awk')
| -rw-r--r-- | runtime/doc/makehtml.awk | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/runtime/doc/makehtml.awk b/runtime/doc/makehtml.awk index 5e40069391..40154b063b 100644 --- a/runtime/doc/makehtml.awk +++ b/runtime/doc/makehtml.awk @@ -58,7 +58,7 @@ substr($0,length($0),1) == "~" { print "<B><FONT COLOR=\"PURPLE\">" substr($0,1, # #ad hoc code # -/^"\|\& / {gsub(/\|/,"\\|"); } +/^"\|& / {gsub(/\|/,"\\|"); } / = b / {gsub(/ b /," \\b "); } # # one letter tag |