Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-07-30 10:40:27 +01:00
Code Issues Projects Releases Packages Wiki Activity

Update devtools page titles.

Browse source
This commit is contained in:
Josh Matthews 2020-04-28 15:40:16 -04:00
parent b53ce5c79a
commit 02ce6188aa
4 changed files with 48 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
components/devtools_traits/lib.rs
View file

@ -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