Revision e3dc6501164ab34d4f94a71be7edd22a78398a9a

Committed on 01/11/2018 5:18 am by Johannes Schmitt <schmittjoh@gmail.com> [GitHub Diff]

fixes dev version