Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-08-02 12:10:29 +01:00
Code Issues Projects Releases Packages Wiki Activity

Add flag to send live updates to devtools.

Browse source
This commit is contained in:
Sagar Muchhal 2015-02-05 19:19:38 +00:00 • committed by Josh Matthews
parent 0beb070d48
commit 5345edf51e
5 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
components/script/devtools.rs
View file

@ -108,3 +108,8 @@ pub fn handle_modify_attribute(page: &Rc<Page>, pipeline: PipelineId, node_id: S
}
}
}
pub fn handle_wants_live_notifications(page: &Rc<Page>, pipeline_id: PipelineId, send_notifications: bool) {
let page = get_page(&*page, pipeline_id);
page.devtools_wants_updates.set(send_notifications);
}