Merge branch 'doc-orig' into doc-debian