Index: src/trusted/service_runtime/osx/run_mig.py |
diff --git a/src/trusted/service_runtime/osx/run_mig.py b/src/trusted/service_runtime/osx/run_mig.py |
index 94aedec3611f551984e4cfc664289817ac93c838..0b508e8fbb7087e2495b7799b06489a4a680204b 100644 |
--- a/src/trusted/service_runtime/osx/run_mig.py |
+++ b/src/trusted/service_runtime/osx/run_mig.py |
@@ -83,10 +83,13 @@ def Generate(src_defs, dst_header, dst_server): |
def Main(args): |
- if len(args) != 3: |
+ if len(args) != 4 and len(args) != 5: |
sys.stderr.write( |
- 'USAGE: %s <src.defs> <dst_header> <dst_server>\n' % sys.argv[0]) |
+ 'USAGE: %s <src.defs> <dst_header> <dst_server> [DEVELOPER_DIR] \n' |
+ % sys.argv[0]) |
sys.exit(1) |
+ if len(args) == 5: |
+ os.environ['DEVELOPER_DIR'] = sys.argv[4] |
Mark Seaborn
2016/10/06 18:27:56
Should be "args[3]" for consistency, rather than u
erikchen
2016/10/06 20:46:22
Done.
|
Generate(args[0], args[1], args[2]) |