HTMLSelectElement.options should be an HTMLOptionsCollection, not HTMLCollection

[evmar]

According to
https://developer.mozilla.org/en-US/docs/Web/API/HTMLSelectElement
the options property should be an HTMLOptionsCollection
https://developer.mozilla.org/en-US/docs/Web/API/HTMLOptionsCollection

Which is just like an HTMLCollection but all the options are HTMLOptionElement.
This allows code like

let select: HTMLSelectElement = ...;
console.log(select.options[0].value);

to work without needing to coerce select.options[0] to a HTMLOptionElement.

See also this (closed) issue for some background -- I think the type of this got a bit funky at one point due to a bug in Edge that was fixed: #1558

[evmar]

This is fixed already.
https://github.com/Microsoft/TypeScript/blob/906ce18b1b5c45374d2bb317f9c707e448c17b55/lib/lib.dom.d.ts#L6791