diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-08-01 22:25:35 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-01 22:25:35 +0200 |
| commit | 89bf19804b87190d1e0e686c9772d9b164acbb88 (patch) | |
| tree | 5c119cf3eb7ea0dfdcd9ecc4d2279102b7a0a5cd /thirdparty | |
| parent | edd69de1fd1cbb9374c9dd77526c0b2dac964d7d (diff) | |
| parent | cd8feed0df5dd765a53c447ff70f59a8518c240c (diff) | |
Merge pull request #10006 from djrm/pr_theme_fixes
Some theme and usability improvements
Diffstat (limited to 'thirdparty')
0 files changed, 0 insertions, 0 deletions