From cf3b75c6875d1bbb8409ff16d9570a8ec52ef197 Mon Sep 17 00:00:00 2001
From: Ben Gras <ben@minix3.org>
Date: Sun, 3 Jul 2011 15:01:18 +0200
Subject: [PATCH] tools/Makefile: don't install servers (workaround)

   . if the build target is invoked again for the install target, the
     stack sizes aren't set properly. A workaround is to only build
     and not install the servers. (Installing them doesn't really make
     sense anyway.)
---
 tools/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/Makefile b/tools/Makefile
index 6c496e9a0..52ef830e6 100644
--- a/tools/Makefile
+++ b/tools/Makefile
@@ -87,7 +87,7 @@ kernel: includes
 	$(MAKE) -C ../kernel 
 
 servers: includes
-	$(MAKE) -C ../servers all install
+	$(MAKE) -C ../servers all
 
 drivers: includes servers
 	$(MAKE) -C ../drivers all install