diff options
| author | Hugo Herbelin | 2018-11-06 22:31:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-06 22:36:16 +0100 |
| commit | 8269e295b07f0fc187c054db3675d5832afd5627 (patch) | |
| tree | c3ff6032a9a466c1b4f55061c495f2a46bb493fe /dev/ci/docker | |
| parent | 92d1a0c14ef326929b6870541073bcae4d2c895d (diff) | |
Fixes #8910 (typo in nameops.ml).
[ci skip]
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions