diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-07-17 22:36:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-07-17 22:36:00 +0200 |
| commit | 2b8342e308762d8621b8866669797f9fab2da873 (patch) | |
| tree | a419f3d0bdb347169554633b60798db848afb7a6 /editor/plugins/theme_editor_plugin.h | |
| parent | 1c1d43ef214f6a8132e8c9a708bf11c0c0192f81 (diff) | |
| parent | a3c2d9a6bdbe3967c8f747e39b2b581729b492c1 (diff) | |
Merge pull request #9652 from djrm/theme_fixes
Improvements and fixes for the default theme.
Diffstat (limited to 'editor/plugins/theme_editor_plugin.h')
0 files changed, 0 insertions, 0 deletions