We now build a docker base container based on debian sid (where the very
latest packages are available). That base container is updated once a
month, or whenever travis-build.Dockerfile or debian/control change, but
re-used for subsequent travis runs. While the initial build might take
up to 15 minutes, subsequent builds typically run in a minute or two.
All the different steps that we run on travis are now factored into
separate scripts in the travis/ directory.
Switching to docker should also help with issue #2174.
This patch moves the title_format information from windows to containers.
Furthermore, it allows correctly setting it on window-less containers and
displays the title accordingly for split containers.
We now also dump and read title_format in GET_TREE / during restarts.
fixes#2120
Michael Stapelberg