Merge branch 'devel' into 'devel'

update devel

See merge request humanoid-path-planner/hpp-doc!12
6 jobs for devel in 191 minutes and 53 seconds (queued for 6 seconds)