We have had a chaotic day, with branches improperly merged into each other. This has created a right mess.Please do not push any commits anywhere except your own private branches.
It will likely take several more hours of work to be sure that everything is as it should be.Please continue to hold all commits to my branches. I'll let you know when devel is back open.