From 43f4e42681c4bc170cf36f38e61e1b7f03be1c43 Mon Sep 17 00:00:00 2001
From: pbrier <git@pbrier.nl>
Date: Thu, 17 Oct 2013 23:22:26 +0200
Subject: [PATCH] Added command line source/build directory option

---
 workspace_tools/make.py | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/workspace_tools/make.py b/workspace_tools/make.py
index 2abca9a22b..30ad2fed36 100644
--- a/workspace_tools/make.py
+++ b/workspace_tools/make.py
@@ -50,6 +50,10 @@ if __name__ == '__main__':
                       default=False, help="Verbose diagnostic output")
     
     # Local run
+    parser.add_option("--source", dest="input_dir",
+                      default=None, help="The source input directory")
+    parser.add_option("--build", dest="output_dir",
+                      default=None, help="The binary output directory")
     parser.add_option("-d", "--disk", dest="disk",
                       default=None, help="The mbed disk")
     parser.add_option("-s", "--serial", dest="serial",
@@ -108,6 +112,10 @@ if __name__ == '__main__':
         test.dependencies.append(RTOS_LIBRARIES)
     
     build_dir = join(BUILD_DIR, "test", mcu, toolchain, test.id)
+    if options.input_dir is not None: 
+        test.source_dir = options.input_dir
+    if options.output_dir is not None: 
+        build_dir = options.output_dir
     
     target = TARGET_MAP[mcu]
     try: