Speed up website build

It turns out that we only need bare HTML files for .md files in news,
yet publish.sh creates them unconditionally. That is, we spend a lot
of time building bare HTML files that we never use.

This commit makes it so that bare HTML files are only generated for
news files, which speeds up the website build significantly:

	$ /home/michael/benchmark.sh speed-up-build master
	Already on 'speed-up-build'

	NOW TESTING ON speed-up-build

	0m08.24s real     0m08.53s user     0m05.57s system
	0m08.21s real     0m08.39s user     0m05.58s system
	0m08.26s real     0m08.23s user     0m05.70s system
	0m08.26s real     0m08.27s user     0m05.91s system
	0m08.24s real     0m08.36s user     0m05.63s system
	0m08.28s real     0m08.40s user     0m05.67s system
	0m08.29s real     0m08.21s user     0m05.83s system
	0m08.23s real     0m08.12s user     0m05.80s system
	0m08.32s real     0m08.32s user     0m05.75s system
	0m08.30s real     0m08.40s user     0m05.61s system

	Switched to branch 'master'
	Your branch is ahead of 'origin/master' by 33 commits.

	NOW TESTING ON master

	0m12.98s real     0m15.07s user     0m07.18s system
	0m12.93s real     0m14.57s user     0m07.69s system
	0m12.98s real     0m15.06s user     0m07.46s system
	0m12.98s real     0m14.75s user     0m07.67s system
	0m12.94s real     0m15.10s user     0m07.22s system
	0m12.94s real     0m14.95s user     0m07.22s system
	0m12.98s real     0m14.57s user     0m08.02s system
	0m12.96s real     0m14.84s user     0m07.41s system
	0m12.96s real     0m14.99s user     0m07.49s system
	0m13.06s real     0m14.91s user     0m07.54s system

And here's the script in question, benchmark.sh:

	#!/bin/sh

	set -u
	set -e

	# usage: runit branch
	runit() {
		git checkout "$1"
		echo
		echo NOW TESTING ON "$1"
		echo
		for i in `jot 10`; do make clean >/dev/null; time make -j2 >/dev/null; done
	}

	make clean >/dev/null

	for branch in "$@"
	do
		runit "$branch"
	done

0 files changed, 0 insertions, 0 deletions