Build was broken by mistake in commit d40662edc41a5a4d09ae690b640cfdeeb24e15a1 Fixes #7362 Signed-off-by: Brice Goglin <Brice.Goglin@inria.fr> (cherry picked from commit 907ad854b46b42ae7cb1e9c87238691a5cc25e36)