diff options
| author | Josh Matthews <josh@joshmatthews.net> | 2020-04-28 15:40:16 -0400 |
|---|---|---|
| committer | Josh Matthews <josh@joshmatthews.net> | 2020-04-28 15:40:38 -0400 |
| commit | 02ce6188aa967ef1722155f9b170183a01a14064 (patch) | |
| tree | 25ed79568348b6cf4f5c944021599bb9c901bd07 /components/devtools_traits/lib.rs | |
| parent | b53ce5c79a6744d24002467e1ff7b7b80e169f36 (diff) | |
| download | servo-02ce6188aa967ef1722155f9b170183a01a14064.tar.gz servo-02ce6188aa967ef1722155f9b170183a01a14064.zip | |
Update devtools page titles.
Diffstat (limited to 'components/devtools_traits/lib.rs')
| -rw-r--r-- | components/devtools_traits/lib.rs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/components/devtools_traits/lib.rs b/components/devtools_traits/lib.rs index 2ac1cae598a..7196c3a5b32 100644 --- a/components/devtools_traits/lib.rs +++ b/components/devtools_traits/lib.rs @@ -97,6 +97,9 @@ pub enum ScriptToDevtoolsControlMsg { /// Report a page error for the given pipeline ReportPageError(PipelineId, PageError), + + /// Report a page title change + TitleChanged(PipelineId, String), } /// Serialized JS return values |