@@ -205,6 +205,24 @@ function addReceivers(ports) {
205 if (v.length > 0) window.location = v;
205 if (v.length > 0) window.location = v;
208+ if ('favicon' in ports) {
209+ if (typeof ports.favicon === 'string') {
210+ changeFavicon(ports.favicon);
212+ ports.favicon.subscribe(changeFavicon);
215+ function changeFavicon(src) {
216+ var link = document.createElement('link');
217+ var oldLink = document.getElementById('elm-favicon');
218+ link.id = 'elm-favicon';
219+ link.rel = 'shortcut icon';
222+ document.head.removeChild(oldLink);
224+ document.head.appendChild(link);
210function initGraphics(elm, Module) {
228function initGraphics(elm, Module) {