diff options
| author | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
| commit | dde10a9b2512ffc7e941c79bbc442c5b4b1f45f9 (patch) | |
| tree | c7e4cbb5b690aaea3a9dedfd516e252fea2ea435 /dev | |
| parent | c45f079c52524da687dfcc9e5f5511d6e86bc537 (diff) | |
| parent | 882e37cfa843ff7444525550e7ac3fe44b1fcecb (diff) | |
Merge PR #11070: Do not rely on the user settings but on the actual window size. (Fixes #10956)
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions