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..763ab4b9dd2418924cf3f0e81b7d5d13343b3b7f 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) != 3 and len(args) != 4: |
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) == 4: |
+ os.environ['DEVELOPER_DIR'] = args[3] |
Generate(args[0], args[1], args[2]) |