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.)

diff --git a/tools/Makefile b/tools/Makefile
index 6c496e9a099535fe6c997962fcbb27e683dfc71f..52ef830e650c44ebe6e82f79c2dddf0d8a9b940b 100644 (file)
--- 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