diff -uNr xenomai/ksrc/drivers/benchmark/timerbench.c xenomai-wd/ksrc/drivers/benchmark/timerbench.c
--- xenomai/ksrc/drivers/benchmark/timerbench.c 2006-01-04 16:22:05.000000000 +0100
+++ xenomai-wd/ksrc/drivers/benchmark/timerbench.c      2006-01-04 17:23:00.000000000 +0100
@@ -18,7 +18,9 @@

 #include <linux/module.h>
 #include <asm/semaphore.h>
-#include <linux/ipipe_trace.h>
+#ifdef CONFIG_IPIPE_TRACE
+ #include <linux/ipipe_trace.h>
+#endif /* CONFIG_IPIPE_TRACE */

 #include <xenomai/rtdm/rtbenchmark.h>
 #include <xenomai/rtdm/rtdm_driver.h>