diff options
| author | Kartik K. Agaram <vc@akkartik.com> | 2016-12-26 01:17:01 -0800 |
|---|---|---|
| committer | Kartik K. Agaram <vc@akkartik.com> | 2016-12-26 01:26:16 -0800 |
| commit | e5c11a5137d538b7713dd8708ca767c208824c06 (patch) | |
| tree | 82976fd80e5d8048840701c351827730b29f89f6 /update_html | |
| parent | 63e1c465e46502bd7c391e31db73e7e5ae19adfd (diff) | |
| download | mu-e5c11a5137d538b7713dd8708ca767c208824c06.tar.gz | |
3709 - line numbers in html
Each line number also gets an anchor name, but I'm not hyperlinking them for now because I don't want to encourage bookmarking these links just yet. They aren't permalinks because every revision may change what's at any given line number.
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 |