From f7a7db83eff079d0494ded92fd73403d23a55538 Mon Sep 17 00:00:00 2001 From: Kartik Agaram Date: Sat, 26 Jun 2021 08:39:05 -0700 Subject: [PATCH] . Drop some long-obsolete tooling. I no longer use iTerm2. --- tools/update_html | 6 ------ 1 file changed, 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