From: Wei Liu <wei.liu2@citrix.com>
Date: Wed, 9 Mar 2016 18:59:47 +0000 (+0000)
Subject: Config.mk: use MINI_OS if specified
X-Git-Url: http://xenbits.xensource.com/gitweb?a=commitdiff_plain;h=2c6420cf811a7ccef0f92d51afa80c569d6885f2;p=people%2Fliuw%2Fmini-os.git

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 e5d8ade..788b0cb 100644
--- 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),)