diff options
| author | Théo Zimmermann | 2017-07-11 17:00:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-07-11 17:24:38 +0200 |
| commit | 8d895c065b9a3dc9cc54b0cbc0f6f8daf275ece4 (patch) | |
| tree | 45459aaeefa727b76cd7ffa98da23e28f6ea5950 /plugins/syntax/string_syntax.ml | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
[travis] Display info on tested commit for PR builds.
This is made necessary by the fact that the displayed commit in the header
of the build can be outdated if the build was restarted or took a long time
to start. Sometimes, it is so old that the link to GitHub is a 404.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions