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 /engine | |
| parent | 965048aa0d4eef1d3933aeb7582c23c78ba838f7 (diff) | |
| parent | 8269e295b07f0fc187c054db3675d5832afd5627 (diff) | |
Merge PR #8928: Fixes #8910: typo in nameops.ml
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/nameops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/nameops.ml b/engine/nameops.ml index 735a59fe51..15e201347c 100644 --- a/engine/nameops.ml +++ b/engine/nameops.ml @@ -69,7 +69,7 @@ let root_of_id id = [bar0] ↦ [bar1] [bar00] ↦ [bar01] [bar1] ↦ [bar2] - [bar01] ↦ [bar01] + [bar01] ↦ [bar02] [bar9] ↦ [bar10] [bar09] ↦ [bar10] [bar99] ↦ [bar100] |