diff options
| author | John MacFarlane <jgm@berkeley.edu> | 2015-01-12 20:09:40 -0800 |
|---|---|---|
| committer | John MacFarlane <jgm@berkeley.edu> | 2015-01-12 20:12:30 -0800 |
| commit | f6de5eb2e20454b0bff875d6e78d76bf5c93a86d (patch) | |
| tree | 14ee4fc65a5e2fc38011b66409cdbcd9a5293d0b /man | |
| parent | 3e6afcb30b9378d3cafc14d8cb2fca2930c244ac (diff) | |
Simplified release archive.
We now simply use git archive (which is also what github would
use on their releases page).
This is possible because we now include some generated files in
the repository.
The fact is that this is what people are going to use anyway,
so instead of testing two different setups (our hand-crafted
archive and the git repo), it's better just to use one.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions