Allow to set a fixed port for the development server.

mojo/devtools/common/devtoolslib/shell_config.py

Index: mojo/devtools/common/devtoolslib/shell_config.py
diff --git a/mojo/devtools/common/devtoolslib/shell_config.py b/mojo/devtools/common/devtoolslib/shell_config.py
index 227b9794526ff6246668a682884838fe301a4497..6a93cb06d206d1294569ef609e541fc80c2ab0d0 100644
--- a/mojo/devtools/common/devtoolslib/shell_config.py
+++ b/mojo/devtools/common/devtoolslib/shell_config.py
@@ -48,6 +48,7 @@ class DevServerConfig(object):
   """
   def __init__(self):
     self.host = None
+    self.port = None
     self.mappings = None
 
 
@@ -193,6 +194,7 @@ def get_shell_config(script_args):
         for dev_server_spec in config['dev_servers']:
           dev_server_config = DevServerConfig()
           dev_server_config.host = dev_server_spec['host']
+          dev_server_config.port = dev_server_spec.get('port', None)
           dev_server_config.mappings = []
           for prefix, path in dev_server_spec['mappings']:
             dev_server_config.mappings.append((prefix, path))