Merge branch 'master' into pure-ops pure-ops
Lukas Mai [Sun, 24 Jun 2012 11:05:55 +0000 (13:05 +0200)]

Trivial merge