From 0cbf3a9ff738be12fcedbabe0c4a06ad9c8a9bb5 Mon Sep 17 00:00:00 2001
From: Alex <158320970+alexb-harmonic@users.noreply.github.com>
Date: Wed, 24 Dec 2025 01:59:29 +0000
Subject: [PATCH] chore: tiny typo in  lake globs syntax

---
 Manual/BuildTools/Lake/Config.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Manual/BuildTools/Lake/Config.lean b/Manual/BuildTools/Lake/Config.lean
index 339a9b4bd..3a65eb3f0 100644
--- a/Manual/BuildTools/Lake/Config.lean
+++ b/Manual/BuildTools/Lake/Config.lean
@@ -1043,7 +1043,7 @@ The glob pattern `N.*` matches `N` or any submodule for which `N` is a prefix.
 $_:name".*"
 ```
 
-The glob pattern `N.*` matches any submodule for which `N` is a strict prefix, but not `N` itself.
+The glob pattern `N.+` matches any submodule for which `N` is a strict prefix, but not `N` itself.
 
 ```grammar
 $_:name".+"