.

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

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