From 22c741bfb6f1f40081cf64210cc87bd7551afb15 Mon Sep 17 00:00:00 2001
From: Frederic Junod <frederic.junod@camptocamp.com>
Date: Wed, 16 Mar 2016 12:28:28 +0100
Subject: [PATCH] Fix HTMLVideoElement.prototype.{width,height} type

See https://www.w3.org/TR/html5/embedded-content-0.html#the-video-element
---
 externs/browser/html5.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/externs/browser/html5.js b/externs/browser/html5.js
index 9bdc6d48f54..8e0bda257c8 100644
--- a/externs/browser/html5.js
+++ b/externs/browser/html5.js
@@ -1697,10 +1697,10 @@ HTMLVideoElement.prototype.webkitExitFullscreen = function() {};
  */
 HTMLVideoElement.prototype.webkitExitFullScreen = function() {};
 
-/** @type {string} */
+/** @type {number} */
 HTMLVideoElement.prototype.width;
 
-/** @type {string} */
+/** @type {number} */
 HTMLVideoElement.prototype.height;
 
 /** @type {number} */