4 Commits

Author	SHA1	Message	Date
Daniel Martí	377199d241	Follow-up to 5a0129d8: also replace file mentions	2015-08-29 20:19:32 -07:00
Hans-Christoph Steiner	93adee0e2b	do not include timestamps in .gz files of docs ... The timestamps in the .gz files are not used for anything, and they break the reproducibility of the build. Giving --no-name means gzip will not save the filename and timestamp in the gz file itself. When gunziping, the current file name will be used, minus the .gz suffix.	2014-10-23 14:26:11 -04:00
Daniel Martí	13cbb7949e	Update gendocs from 2011-04 to 2013-02	2013-12-30 16:33:42 +01:00
Ciaran Gultnieks	9ca42ec9f4	Manual in lots of formats	2012-02-25 08:30:43 +00:00