propagate EXTRA_OPTS

diff --git a/servers/Makefile b/servers/Makefile
index 07bd4f11de90a4513ec97602162ef58428084c4f..8e0852c81e9ced65bb0a35915b442351b163c22d 100644 (file)
--- a/servers/Makefile
+++ b/servers/Makefile
@@ -23,9 +23,9 @@ all install depend clean:
        cd ./inet && $(MAKE) $@
 
 image:
-       cd ./pm && $(MAKE) build
-       cd ./fs && $(MAKE) build
-       cd ./rs && $(MAKE) build
-       cd ./init && $(MAKE) build
+       cd ./pm && $(MAKE) EXTRA_OPTS=$(EXTRA_OPTS) build
+       cd ./fs && $(MAKE) EXTRA_OPTS=$(EXTRA_OPTS) build
+       cd ./rs && $(MAKE) EXTRA_OPTS=$(EXTRA_OPTS) build
+       cd ./init && $(MAKE) EXTRA_OPTS=$(EXTRA_OPTS) build