Hi all, we are changing git branching politics. :) As you can see, I have merged devel branch into master branch. Master will be used for development from now. If we need to keep track of some stable release, we will create new branch for it. (hope it's clear ;) ) Peter.