diff options
| author | Maxime Dénès | 2017-07-17 07:34:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-17 07:34:32 +0200 |
| commit | a14a894870b9503e649bb79f32a26a6b9171f02a (patch) | |
| tree | c0894b4af834d1e75ef8e5fc676775f2d7799c5c /plugins/syntax/string_syntax.ml | |
| parent | e3c4da34f14b00d2b3feb087fcce1cebd8064064 (diff) | |
| parent | 8d895c065b9a3dc9cc54b0cbc0f6f8daf275ece4 (diff) | |
Merge PR #872: [travis] Display info on tested commit for PR builds.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions