chiark / gitweb /
Merge branch 'miscfixes' into 'master'
authorTorsten Grote <t+gitlab@grobox.de>
Tue, 4 Apr 2017 21:28:08 +0000 (21:28 +0000)
committerTorsten Grote <t+gitlab@grobox.de>
Tue, 4 Apr 2017 21:28:08 +0000 (21:28 +0000)
misc fixes

Closes #268

See merge request !245


Trivial merge