| Wed, 29 Aug 2012 20:54:49 +0200 | wenzelm | one more round to ensure that base images are already there, without producing document output themselves; | file | diff | annotate |
| Tue, 28 Aug 2012 20:10:53 +0200 | wenzelm | prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools; | file | diff | annotate |
| Tue, 28 Aug 2012 17:49:02 +0200 | wenzelm | more formal build_doc tool (Admin only); | file | diff | annotate |