mirror of
https://github.com/servo/servo.git
synced 2025-08-03 12:40:06 +01:00
Add support for launching devtools server on random port
Assign random port to devtools server in case user does not specify a port explicitly and report it to the embedding layer for display to user.
This commit is contained in:
parent
6ab923c8e8
commit
94db0d61cb
10 changed files with 73 additions and 9 deletions
|
@ -198,6 +198,8 @@ pub enum EmbedderMsg {
|
|||
/// Notifies the embedder about media session events
|
||||
/// (i.e. when there is metadata for the active media session, playback state changes...).
|
||||
MediaSessionEvent(MediaSessionEvent),
|
||||
/// Report the status of Devtools Server
|
||||
OnDevtoolsStarted(Result<u16, ()>),
|
||||
}
|
||||
|
||||
impl Debug for EmbedderMsg {
|
||||
|
@ -232,6 +234,7 @@ impl Debug for EmbedderMsg {
|
|||
EmbedderMsg::BrowserCreated(..) => write!(f, "BrowserCreated"),
|
||||
EmbedderMsg::ReportProfile(..) => write!(f, "ReportProfile"),
|
||||
EmbedderMsg::MediaSessionEvent(..) => write!(f, "MediaSessionEvent"),
|
||||
EmbedderMsg::OnDevtoolsStarted(..) => write!(f, "OnDevtoolsStarted"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue