fix compilation problem on linux

2 jobs for master in 17 seconds (queued for 3 seconds)
Status Job ID Name Coverage
  Configure
passed #104637
linux
configure-linux

00:00:02

 
  Compile
passed #104638
linux
make-linux

00:00:14