diff options
| author | John MacFarlane <jgm@berkeley.edu> | 2014-08-17 17:33:07 -0700 |
|---|---|---|
| committer | John MacFarlane <jgm@berkeley.edu> | 2014-08-17 17:33:07 -0700 |
| commit | 31cca8ff6df2a2d3d37be629ef1defdbf35202c3 (patch) | |
| tree | c9e109a7dda5a2a1b18ee49eb1dd683917ebee48 | |
| parent | bee40280e2ce7afeda147586de3d2cdaf4d15d25 (diff) | |
update-site: Don't copy README.html to index.html.
We'll make index.html a separate document.
| -rw-r--r-- | Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -60,7 +60,6 @@ fuzztest: time cat /dev/urandom | head -c 100000 | iconv -f latin1 -t utf-8 | $(PROG) >/dev/null; done update-site: README.html spec.html - cp README.html _site/index.html cp spec.html _site/ cp -r js/* _site/js/ |