diff options
| author | Kartik Agaram <vc@akkartik.com> | 2018-05-12 10:22:26 -0700 |
|---|---|---|
| committer | Kartik Agaram <vc@akkartik.com> | 2018-05-12 10:22:26 -0700 |
| commit | cdf2822743b3beeb37ebc3deea8e08b6130698c5 (patch) | |
| tree | b7946314d79e8df95eb16703b65832e20f7ee620 /update_html | |
| parent | bd222553d7bc7d91d3eebae5639b01f58c8f7c75 (diff) | |
| download | mu-cdf2822743b3beeb37ebc3deea8e08b6130698c5.tar.gz | |
4242 - get rid of refcounts entirely
We're going to lean back into the experiment of commit 4179 back in Jan. If we delete memory it's up to us to ensure no pointers into it survive. Since deep-copy depends on our refcounting infrastructure, it's gone as well. So we're going to have to start watching out for pointers shared over channels.
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 |