Merge tag 'debian/7.0' into stretch-bpo

dgit release 7.0 for unstable (sid) [dgit]
[dgit distro=debian]

# gpg: Signature made Thu 04 Oct 2018 12:36:14 PM MST
# gpg:                using RSA key 559AE46C2D6B6D3265E7CBA1E3E3392348B50D39
# gpg: Can't check signature: No public key

1 files changed, 27 insertions, 0 deletions

diff --git a/po4a/install-documents b/po4a/install-documents
new file mode 100755
index 0000000..138c88e
--- /dev/null
+++ b/po4a/install-documents
@@ -0,0 +1,27 @@
+#!/bin/bash
+set -e
+
+srcdir=$1; shift
+destdir=$1; shift
+
+mkdir -p "$srcdir"
+
+docs=( $( ( cd "$srcdir" && find man -type f ) | sed 's#\.pod$##' ) )
+
+echo ${docs[*]}
+
+x () {
+	echo "+ $*";
+	"$@"
+}
+
+if [ "${#docs}" = 0 ]; then exit 0; fi
+
+x ${MAKE-make} -s -C "$srcdir" -f ../../Makefile ${docs[@]}
+
+mandest=$destdir/usr/share
+
+for f in "${docs[@]}"; do
+	mkdir -p "$mandest/${f%/*}"
+	x cp "$srcdir/$f" "$mandest/$f"
+done