Fix failing raspberry pi builds
The branch had passed in dev because I had already done this fix
I missed pushing the commit to gitlab.com and the MR got merged without it
Edited by GitLab Release Tools Bot
The branch had passed in dev because I had already done this fix
I missed pushing the commit to gitlab.com and the MR got merged without it