diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-09-25 23:02:50 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-25 23:02:50 +0200 |
| commit | 25264568076c4aaea1319c941fdc64bd28d4c078 (patch) | |
| tree | a40f4cdecc2279288d4cc0858f8fde0087122bd6 /editor/plugins | |
| parent | 78aa7b382a8b1c80e0e2b01e02ff0acb2942e2e1 (diff) | |
| parent | 5676c42ae02f995b7915edc8afe3de9a73ebecfc (diff) | |
Merge pull request #11564 from djrm/pr_editor_settings_undo
Added the ability to revert to initial value in editor settings.
Diffstat (limited to 'editor/plugins')
0 files changed, 0 insertions, 0 deletions