diff options
Diffstat (limited to 'update_html')
| -rwxr-xr-x | update_html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/update_html b/update_html index 651b287f..d525ee8d 100755 --- a/update_html +++ b/update_html @@ -16,7 +16,7 @@ process() { convert_html() { vim -c "set number" -c TOhtml -c write -c qall $1 - sed -i 's,<title>\~/mu/,<title>Mu - ,' $1.html + sed -i 's,<title>.*/mu/,<title>Mu - ,' $1.html sed -i 's,\.html</title>,</title>,' $1.html sed -i 's/^\* { \(.*\) }/* { font-size: 12pt; \1 }/g' $1.html sed -i 's/^body { \(.*\) }/body { font-size: 12pt; \1 }/g' $1.html |