work around slim image not providing /usr/share/man

Work around debian slim image not providing /usr/share/man, and postgresql's
postinst failing because those directories do not exist.

diff --git a/.travis/Dockerfile b/.travis/Dockerfile
index 36c94d509b8e14f5ea0ec4967052ccf6dd66e6ff..c5fbffa5a4152d848b50ca1543efcdd300b52476 100644 (file)
--- a/.travis/Dockerfile
+++ b/.travis/Dockerfile
@@ -16,6 +16,8 @@ RUN echo '\nPackage: *\nPin: release a=unstable\nPin-Priority: 1\n\n'\
  >> /etc/apt/preferences
 RUN echo '\nPackage: *\nPin: release a=stretch-backports\nPin-Priority: 500\n\n'\
  >> /etc/apt/preferences
+# work around slim image interacting with missing documentation
+RUN for a in $(seq 1 7); do mkdir -p /usr/share/man/man$a; done;
 RUN apt-get -qq update && \
  mk-build-deps --install \
  --tool 'apt-get -y -o Debug:pkgProblemResolver=yes --no-install-recommends' \