mirror of
https://github.com/servo/servo.git
synced 2025-08-26 23:58:20 +01:00
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. This is done by getopts and is the same for other such options, e.g. `--profile`.
This commit is contained in:
parent
94731270df
commit
8a5c6a0d3b
4 changed files with 21 additions and 19 deletions
|
@ -68,7 +68,7 @@ pub extern "C" fn cef_run_message_loop() {
|
|||
show_debug_borders: false,
|
||||
enable_text_antialiasing: true,
|
||||
trace_layout: false,
|
||||
devtools_server: false,
|
||||
devtools_port: None,
|
||||
initial_window_size: TypedSize2D(800, 600),
|
||||
user_agent: None,
|
||||
};
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue