Merge branch 't/gui_reload_fix'
authorAndre Noll <maan@tuebingen.mpg.de>
Sun, 22 Mar 2015 20:45:11 +0000 (21:45 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Sun, 22 Mar 2015 20:45:11 +0000 (21:45 +0100)
Was cooking for two weeks.

* t/gui_reload_fix:
  gui: Fix config file reloading.


Trivial merge