restore 16280fad7b90f41b4b43c90371e35b35c92b6b25
Seems the merge of master into master was correct and the revert done in 75d1438eb15719b23f7101dfe76bcbd9d2e3d08d was not.
Probably all that was the result of me not using anongit at all cause of the performance and push problems we had? Maybe
somehow that resulted now in two repos not being in sync? Well, who knows :-/ Let's hope it doesn't happen that often.