gui: Remove unused widgets.
authorAndre Noll <maan@tuebingen.mpg.de>
Mon, 1 Sep 2014 21:53:19 +0000 (23:53 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Sat, 27 Sep 2014 23:01:59 +0000 (23:01 +0000)
commited9be5dbf52b45497838034033e210ce984c17a6
tree0e47671b247db33d449d51c2417566756e4907ce
parent521b9d7584ff363b9af24f33e0afb1e954da854a
gui: Remove unused widgets.

No application uses these public functions, so remove them for now.
They can be re-added on demand but for now they are just dead code.
gui