Fix compilation with gcc 5.4 (Ubuntu 16.04)
Although we do not officially support Ubuntu 16.04, it's nice to keep it working.
It was broken by !579 (merged).
Edited by Marco Clemencic
Although we do not officially support Ubuntu 16.04, it's nice to keep it working.
It was broken by !579 (merged).