diff options
| author | bors-servo <lbergstrom+bors@mozilla.com> | 2018-08-07 06:51:09 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-07 06:51:09 -0400 |
| commit | e363d579fa3fbceb4659d9128f800571750087d6 (patch) | |
| tree | 92c14b9a9785ceef6e6ac93745bcc3830333fa46 /python/servo/devenv_commands.py | |
| parent | 2a0eec4ad6e6e066f2fcf910e29632ef19914abf (diff) | |
| parent | 4dfe617d3ff24bd694f5ff7686b052c5d2d338e5 (diff) | |
| download | servo-e363d579fa3fbceb4659d9128f800571750087d6.tar.gz servo-e363d579fa3fbceb4659d9128f800571750087d6.zip | |
Auto merge of #21302 - paulrouget:res, r=mbrubeck
Fix page size when device-pixel-ratio is set manually
Fix #21277
We were using the user-define pixel ratio to get the device values of the winit coordinates.
<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/servo/servo/21302)
<!-- Reviewable:end -->
Diffstat (limited to 'python/servo/devenv_commands.py')
0 files changed, 0 insertions, 0 deletions