Future merge master

merge master into future using git merge --commit -Xours -Xignore-space-change origin/master

labelled as WIP: to avoid any possible interference with the hackaton preparations...