diff options
| author | Gaëtan Gilbert | 2018-01-09 16:49:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-01-16 16:27:07 +0100 |
| commit | 5d7e703f643930f2ba90767e75dee01d3e0c6fd6 (patch) | |
| tree | 9af7cc10602784b049a259c242f2cd06ce1ba6f5 /dev/ci | |
| parent | 0be785a5832177efa4ec396a421a4eb367b81914 (diff) | |
merge-pr.sh: use git diff --quiet
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions