diff --git a/tools/Makefile b/tools/Makefile index 1a09c09d6..d8991b713 100644 --- a/tools/Makefile +++ b/tools/Makefile @@ -93,8 +93,13 @@ services: includes kernel servers .WAIT drivers kernel: includes $(MAKE) -C ../kernel +.if ${COMPILER_TYPE} == "gnu" +servers: includes + $(MAKE) -C ../servers all install +.else servers: includes $(MAKE) -C ../servers all +.endif drivers: includes servers $(MAKE) -C ../drivers all install