From ccae45851f729ada29391e7497cf8e4c9796ff8c Mon Sep 17 00:00:00 2001 From: "Kartik K. Agaram" Date: Fri, 25 Nov 2016 11:04:14 -0800 Subject: 3687 --- update_html | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'update_html') diff --git a/update_html b/update_html index 5ca4d74b..54d803d3 100755 --- a/update_html +++ b/update_html @@ -17,6 +17,12 @@ process() { sed -i 's/^\.Identifier .*/.Identifier { color: #c0a020; }/' $1.html # same as muControl sed -i 's/^\.Special .*/.Special { color: #c00000; }/' $1.html # same as traceAbsent.. + # 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 + mv -i $1.html html/`dirname $1` } @@ -35,10 +41,3 @@ for f in *.cc *.mu edit/*.mu do process $f done - -# switch the 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 's/┈/╌/g' html/edit/*.mu.html -sed -i 's/┊/╎/g' html/edit/*.mu.html -- cgit 1.4.1-2-gfad0