Merge branch 'devel' into 'devel'

update pinocchio See merge request !7

Merge branch 'devel' into 'devel'
update pinocchio See merge request !7
445c2168 · Guilhem Saurel · 37ecf74d · db93bebe · 445c2168
Commit 445c2168 authored Jul 28, 2020 by Guilhem Saurel
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

doc/Makefile doc/Makefile +1 -1

No files found.
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -42,7 +42,7 @@ INSTALL_DOCUMENTATION=ON
 ##################################
 # {{{ Dependencies

-pinocchio_branch=v2.4.5
+pinocchio_branch=v2.4.7
 pinocchio_repository=${SOT_REPO}
 pinocchio_extra_flags= -DBUILD_PYTHON_INTERFACE=OFF -DBUILD_UNIT_TESTS=OFF -DBUILD_WITH_COLLISION_SUPPORT=ON