Config.mk: use MINI_OS if specified

Signed-off-by: Wei Liu <wei.liu2@citrix.com>

diff --git a/Config.mk b/Config.mk
index e5d8ade1b5e1913874f333a7068b5669103f4336..788b0cbf5976eb03cd2107eb4f5a414c0982941b 100644 (file)
--- a/Config.mk
+++ b/Config.mk
@@ -31,6 +31,10 @@ MINI-OS_ROOT=$(XEN_ROOT)/extras/mini-os
 else
 MINI-OS_ROOT=$(TOPLEVEL_DIR)
 endif
+# It is also possible that mini-os is specified directly.
+ifneq ($(MINI_OS),)
+MINI-OS_ROOT=$(MINI_OS)
+endif
 export MINI-OS_ROOT
 
 ifneq ($(XEN_TARGET_ARCH),)