.

Drop some long-obsolete tooling. I no longer use iTerm2.

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