Merge branch 'develop' into armv7
authorwernsaar <wernsaar@googlemail.com>
Sun, 1 Dec 2013 09:12:07 +0000 (10:12 +0100)
committerwernsaar <wernsaar@googlemail.com>
Sun, 1 Dec 2013 09:12:07 +0000 (10:12 +0100)

Trivial merge