reducing font size of terminals; push buttons to top
authorStefan Huber <shuber2@gmail.com>
Sun, 8 Jun 2008 17:25:11 +0000 (19:25 +0200)
committerStefan Huber <shuber2@gmail.com>
Sun, 8 Jun 2008 17:25:11 +0000 (19:25 +0200)

No differences found