From 8269e295b07f0fc187c054db3675d5832afd5627 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 6 Nov 2018 22:31:56 +0100
Subject: Fixes #8910 (typo in nameops.ml).

[ci skip]
---
 engine/nameops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

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]
-- 
cgit v1.2.3