diff options
| author | Pierre-Marie Pédrot | 2018-11-07 17:29:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-07 17:29:52 +0100 |
| commit | 9185c2ed45319c2b35da0e7af9d8a9126f8035ed (patch) | |
| tree | 12fcbf606971fe2b26b4900dea27f5d44bbe5190 /dev/ci/docker | |
| parent | 965048aa0d4eef1d3933aeb7582c23c78ba838f7 (diff) | |
| parent | 8269e295b07f0fc187c054db3675d5832afd5627 (diff) | |
Merge PR #8928: Fixes #8910: typo in nameops.ml
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions