diff options
| author | Emilio Jesus Gallego Arias | 2019-03-01 12:20:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-01 12:20:10 +0100 |
| commit | ebdcaa393b1f332ad917b33bf9d7a222d3faa7c4 (patch) | |
| tree | 2a934fdfde29adbddc74f0587e038e159c429cb2 /dune | |
| parent | 2eb10f5a34ddb378051db9e4df943956ac0e3849 (diff) | |
| parent | b46b8cbe886ea1e06377843134e9c588394acc5f (diff) | |
Merge PR #9610: Fix #9110: mention check-owners-pr.sh
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: vbgl
Diffstat (limited to 'dune')
0 files changed, 0 insertions, 0 deletions