servo/servo — pull request #3612 by robinst (2014-10-08 12:35:38+00:00)
Title: Allow to specify port with --devtools option (fixes #3597)

Note that using `servo --devtools http://example.org` doesn't work. In
that case either the port must be specified or the option moved to the
end. But this is the same for other such options, e.g. `--profile`.