diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2017-08-23 00:05:27 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-08-23 00:05:27 +0200 |
| commit | 172519bec6499d2d7b52875c1bfb685c7df2278f (patch) | |
| tree | fb92ae25c7eb7a1405c7805cc2053dba7786a5f1 /editor/doc | |
| parent | 7ed95828894621565e0dd289ea856426ca72e344 (diff) | |
| parent | 1f90f5ed4c767271df9fbbad01594db172f34f3c (diff) | |
Merge pull request #10551 from djrm/pr_editor_fixes
Do not use old styles for tab buttons
[ci skip]
Diffstat (limited to 'editor/doc')
0 files changed, 0 insertions, 0 deletions