chiark / gitweb /
Fix building of documentation when doing out-of-source builds.