Index: tools/config.py
===================================================================
--- tools/config.py	(revision 5f24137d560f5f077807a0a6fd458ec00e5789db)
+++ tools/config.py	(revision a710680c4299b4bf82de04a739448ab83fc1b87f)
@@ -458,4 +458,5 @@
     if len(sys.argv) >= 4:
         defaults['ARCH'] = sys.argv[3]
+        defaults['PLATFORM'] = sys.argv[3]
 	
 	# Get COMPILER from command line if specified