diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-04-04 22:27:21 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-04 22:27:21 +0200 |
| commit | e223702776a7631293426e40d6f8d3a6240bb1b5 (patch) | |
| tree | fde75644b4c9f960c43a2026fe155bbc2c41e675 /platform | |
| parent | 919209907dfcfa1fddaf7cf5f11068f523f8ead5 (diff) | |
| parent | f0db7fca79297d731fa6abe1e345ce26e1758cd4 (diff) | |
Merge pull request #17784 from Rubonnek/rename-shortcut
Added shortcut to rename files
Diffstat (limited to 'platform')
0 files changed, 0 insertions, 0 deletions