diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2020-11-30 09:25:48 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-30 09:25:48 +0100 |
| commit | 78d9aa99cabb47b2f285323e119bbef7972c1822 (patch) | |
| tree | eb971259996025c62055de5ea5ba765c378abc9f /thirdparty/oidn/common | |
| parent | 375cfa0d50d66c40ed96bb5094269bfa052ba31d (diff) | |
| parent | 231231f9040f61ab49b840cd18d0bb9566e304c8 (diff) | |
Merge pull request #43970 from EricEzaM/PR/popup-menu-margin-shrink
Reduced EditorTheme margin on PopupMenu
Diffstat (limited to 'thirdparty/oidn/common')
0 files changed, 0 insertions, 0 deletions