diff options
author | Kunal Mohan <kunalmohan99@gmail.com> | 2020-03-07 20:23:14 +0530 |
---|---|---|
committer | Kunal Mohan <kunalmohan99@gmail.com> | 2020-03-16 15:30:26 +0530 |
commit | 94db0d61cb6a92e36b2047ec6c643b3fa4734789 (patch) | |
tree | 03bd48d6418073fce5da1a21c242d780021513cd /components/embedder_traits/lib.rs | |
parent | 6ab923c8e8172ce1a4944b85cac549fa99ec9f4d (diff) | |
download | servo-94db0d61cb6a92e36b2047ec6c643b3fa4734789.tar.gz servo-94db0d61cb6a92e36b2047ec6c643b3fa4734789.zip |
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.
Diffstat (limited to 'components/embedder_traits/lib.rs')
-rw-r--r-- | components/embedder_traits/lib.rs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/components/embedder_traits/lib.rs b/components/embedder_traits/lib.rs index cacaf80ca50..45fa6e1d7b4 100644 --- a/components/embedder_traits/lib.rs +++ b/components/embedder_traits/lib.rs @@ -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"), } } } |