Merge latest master into panda_clean

"panda_clean" is missing some developments of the master branch.

A good branching strategy is typically to regularly merge the master branch into a side branch.