diff options
| author | Tej Chajed | 2017-08-10 16:25:52 +0100 |
|---|---|---|
| committer | Tej Chajed | 2017-08-10 16:25:52 +0100 |
| commit | 82ac0208b86c8a3a913e10c81208e0716d2d4bcf (patch) | |
| tree | d296f36f406d5eeebb0a52768a6d48a293e4b40b /plugins/syntax/string_syntax.ml | |
| parent | de170f36c9b8e36810126fec82ff9cce2a2af2e7 (diff) | |
Describe pull requests a bit more precisely
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions