| 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 |