diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-10-25 10:55:25 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-25 10:55:25 +0200 |
| commit | 70454767ee2398f398aa04a8354480f3f2748ca2 (patch) | |
| tree | 65f2e47713dc0bd528fea70de0842a6dc2519e7a /doc/tools/doc_merge.py | |
| parent | 220f50e790223c7bc63fd3d2ca3327aa6dcc5d3c (diff) | |
| parent | 3af11ff3d8844f4dccd5df307f9383237e8b9fb7 (diff) | |
Merge pull request #23215 from Chaosus/filedock_update
Updates filesystem dock when theme is changed
Diffstat (limited to 'doc/tools/doc_merge.py')
0 files changed, 0 insertions, 0 deletions