Merge branch 'make-dist-improvements'
authorChristian Herdtweck <christian.herdtweck@intra2net.com>
Thu, 7 Feb 2019 15:45:54 +0000 (16:45 +0100)
committerChristian Herdtweck <christian.herdtweck@intra2net.com>
Thu, 7 Feb 2019 15:53:34 +0000 (16:53 +0100)

Trivial merge