From a1ae9d36df034a24d9eb74bd0499ff1282d2303e Mon Sep 17 00:00:00 2001
From: Gregory Nutt <gnutt@nuttx.org>
Date: Wed, 6 Aug 2014 18:28:51 -0600
Subject: [PATCH] Don't build in sched_processtimer.c if CONFIG_SCHED_TICKLESS
 is selected.

---
 sched/Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/sched/Makefile b/sched/Makefile
index 67da182ab6..26c790c84e 100644
--- a/sched/Makefile
+++ b/sched/Makefile
@@ -119,7 +119,9 @@ ENV_SRCS += env_clearenv.c env_getenv.c env_putenv.c env_setenv.c env_unsetenv.c
 WDOG_SRCS = wd_initialize.c wd_create.c wd_start.c wd_cancel.c wd_delete.c
 WDOG_SRCS += wd_gettime.c
 
-TIME_SRCS = sched_processtimer.c
+ifneq ($(CONFIG_SCHED_TICKLESS),y)
+TIME_SRCS += sched_processtimer.c
+endif
 
 ifneq ($(CONFIG_DISABLE_SIGNALS),y)
 TIME_SRCS += nanosleep.c