///| #external type WebGLRenderingContext