diff options
author | bors-servo <servo-ops@mozilla.com> | 2020-04-28 16:56:11 -0400 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-28 16:56:11 -0400 |
commit | 1aab10f20aa1409ce59577d0d383b8001d440296 (patch) | |
tree | 6da8cff5e19c576b9013730458561787da86c1ef /components/script/dom/document.rs | |
parent | bb7a5b6dba5a9511468b9913922e510a3c49a94c (diff) | |
parent | 02ce6188aa967ef1722155f9b170183a01a14064 (diff) | |
download | servo-1aab10f20aa1409ce59577d0d383b8001d440296.tar.gz servo-1aab10f20aa1409ce59577d0d383b8001d440296.zip |
Auto merge of #26325 - jdm:devtools-nav, r=gterzian
Improve devtools experience when navigating
The primary motivation for this work was to fix #15425, and these changes make it possible to use the devtools to meaningfully inspect multiple pages when navigating between them. Navigating through session history is not yet supported.
These changes also include improvements to the dedicated worker support, which broke at some point. We now can observe console messages in workers.
Diffstat (limited to 'components/script/dom/document.rs')
-rw-r--r-- | components/script/dom/document.rs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/components/script/dom/document.rs b/components/script/dom/document.rs index 2d0f2ce1c26..3606ffc7c9d 100644 --- a/components/script/dom/document.rs +++ b/components/script/dom/document.rs @@ -934,6 +934,14 @@ impl Document { pub fn title_changed(&self) { if self.browsing_context().is_some() { self.send_title_to_embedder(); + let global = self.window.upcast::<GlobalScope>(); + if let Some(ref chan) = global.devtools_chan() { + let title = String::from(self.Title()); + let _ = chan.send(ScriptToDevtoolsControlMsg::TitleChanged( + global.pipeline_id(), + title, + )); + } } } |