theia: set THEIA_MINI_BROWSER_HOST_PATTERN to hostname

This is required for example to preview images (ie. open a .png file from the
editor). Without the default value of {{uuid}}.mini-browser.{{hostname}} is used
but we don't have anything in place to resolve such domain names.

software/theia/buildout.hash.cfg

@@ -15,7 +15,7 @@
 
 [instance-theia]
 _update_hash_filename_ = instance-theia.cfg.jinja.in
-md5sum = 79c340ec9f4af948723ef5201b311f45
+md5sum = 942e269192d284e563a84ae710c0595b
 
 [instance]
 _update_hash_filename_ = instance.cfg.in

software/theia/instance-theia.cfg.jinja.in

@@ -328,6 +328,7 @@ template =
   {{ "{% raw %}" }}
   {% raw %}
   export THEIA_WEBVIEW_EXTERNAL_ENDPOINT='{{hostname}}'
+  export THEIA_MINI_BROWSER_HOST_PATTERN='{{hostname}}'
   {% endraw %}
   {{ "{% endraw %}" }}
   export THEIA_OPEN_EDITOR_TOKEN=$(${openssl:location}/bin/openssl rand -hex 32)