diff options
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] |