diff options
| author | Gaëtan Gilbert | 2018-11-07 14:47:07 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-07 14:47:07 +0100 |
| commit | 8f09c0667d2566534ab9da77651686904b23aac5 (patch) | |
| tree | 37552eab9571e9c984dd6bd21b2f0b02d1404f62 /plugins/syntax | |
| parent | 14c55444b3bd574f77b4443916c55f8f102414b6 (diff) | |
| parent | bf513f66ebf4e33a6c923bff0d0c7828dda58acf (diff) | |
Merge PR #8927: Optimise git cloning
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions