--- src/timing/cl_t_current2.cc.orig	2009-05-10 22:32:32.000000000 +0200
+++ src/timing/cl_t_current2.cc	2017-06-07 15:14:54.972741636 +0200
@@ -20,6 +20,7 @@
   #include <sys/types.h>
   #include <sys/param.h> // defines HZ, unit for times() is 1/HZ seconds
   #include <sys/times.h>
+  #include <linux/param.h>
   extern "C" clock_t times (struct tms * buffer);
 #endif
 #ifdef HAVE_PERROR_DECL