diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/update_html | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/tools/update_html b/tools/update_html index 6fadd0e9..add9a89c 100755 --- a/tools/update_html +++ b/tools/update_html @@ -30,12 +30,6 @@ convert_html() { sed -i 's/^body { \(.*\) }/body { font-size:12pt; \1 }/g' $1.html sed -i '/^body {/a a { color:inherit; }' $1.html - - # switch unicode characters around in the rendered html - # the ones we have in the source files render double-wide in html - # the ones we want in the html cause iTerm2 to slow down in alt-tabbing for some reason - # the following commands give us the best of both worlds - sed -i -e 's/┈/╌/g' -e 's/┊/╎/g' $1.html } ctags -x boot.subx [0-9]*.subx [0-9]*.mu > /tmp/tags |