diff options
Diffstat (limited to 'update_html')
| -rwxr-xr-x | update_html | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/update_html b/update_html index 54d803d3..b0051707 100755 --- a/update_html +++ b/update_html @@ -2,7 +2,10 @@ # Regenerate html files. process() { - vim -c TOhtml -c write -c qall $1 + vim -c "set number" -c TOhtml -c write -c qall $1 + # per-line anchors + sed -i 's/^<span id="\([^"]*\)"/<a name="\1"><\/a>&/' $1.html + sed -i 's/^\.LineNr .*/.LineNr { color: #444444; }/' $1.html sed -i 's,<title>\~/mu/,<title>Mu - ,' $1.html sed -i 's,\.html</title>,</title>,' $1.html |