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 /engine/nameops.ml | |
| parent | 92d1a0c14ef326929b6870541073bcae4d2c895d (diff) | |
Fixes #8910 (typo in nameops.ml).
[ci skip]
Diffstat (limited to 'engine/nameops.ml')
| -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] |