From a139814b2f9c9c8c06d16ff330f523cb005e969f Mon Sep 17 00:00:00 2001
From: Frederic Junod <frederic.junod@camptocamp.com>
Date: Wed, 15 Jan 2014 16:00:36 +0100
Subject: [PATCH] Scale WebGL output canvas by devicePixelRatio

---
 src/ol/renderer/webgl/webglmaprenderer.js | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ol/renderer/webgl/webglmaprenderer.js b/src/ol/renderer/webgl/webglmaprenderer.js
index bacc5b9df3..d2bdb4add3 100644
--- a/src/ol/renderer/webgl/webglmaprenderer.js
+++ b/src/ol/renderer/webgl/webglmaprenderer.js
@@ -473,10 +473,11 @@ ol.renderer.webgl.Map.prototype.renderFrame = function(frameState) {
     layerRenderer.prepareFrame(frameState, layerState);
   }
 
-  var size = frameState.size;
-  if (this.canvas_.width != size[0] || this.canvas_.height != size[1]) {
-    this.canvas_.width = size[0];
-    this.canvas_.height = size[1];
+  var width = frameState.size[0] * frameState.pixelRatio;
+  var height = frameState.size[1] * frameState.pixelRatio;
+  if (this.canvas_.width != width || this.canvas_.height != height) {
+    this.canvas_.width = width;
+    this.canvas_.height = height;
   }
 
   gl.bindFramebuffer(goog.webgl.FRAMEBUFFER, null);