Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-08-02 04:00:32 +01:00
Code Issues Projects Releases Packages Wiki Activity

Avoid selecting on the devtools port if no devtools server exists.

Browse source
This commit is contained in:
Josh Matthews 2014-09-02 22:10:26 -04:00
parent bb9955c281
commit c31e2f928d
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
components/script/script_task.rs
View file

@ -162,7 +162,7 @@ pub struct ScriptTask {
compositor: Box<ScriptListener>, compositor: Box<ScriptListener>,
/// For providing instructions to an optional devtools server. /// For providing instructions to an optional devtools server.
_devtools_chan: Option<DevtoolsControlChan>, devtools_chan: Option<DevtoolsControlChan>,
/// For receiving commands from an optional devtools server. Will be ignored if /// For receiving commands from an optional devtools server. Will be ignored if
/// no such server exists. /// no such server exists.
devtools_port: DevtoolsControlPort, devtools_port: DevtoolsControlPort,
@ -332,7 +332,7 @@ impl ScriptTask {
control_port: control_port, control_port: control_port,
constellation_chan: constellation_chan, constellation_chan: constellation_chan,
compositor: compositor, compositor: compositor,
_devtools_chan: devtools_chan, devtools_chan: devtools_chan,
devtools_port: devtools_receiver, devtools_port: devtools_receiver,
js_runtime: js_runtime, js_runtime: js_runtime,
@ -430,7 +430,9 @@ impl ScriptTask {
unsafe { unsafe {
port1.add(); port1.add();
port2.add(); port2.add();
port3.add(); if self.devtools_chan.is_some() {
port3.add();
}
} }
let ret = sel.wait(); let ret = sel.wait();
if ret == port1.id() { if ret == port1.id() {