From 33b609abd965728b7ba4c86487596415caa51725 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 26 Sep 2024 15:09:05 +0200 Subject: [PATCH] introduce typo --- scripts/autolabel.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/autolabel.lean b/scripts/autolabel.lean index ccf7d7321c35e..cfc9a1f52bb21 100644 --- a/scripts/autolabel.lean +++ b/scripts/autolabel.lean @@ -89,7 +89,7 @@ def mathlibLabels : Array Label := #[ "Mathlib" / "RingTheory", "Mathlib" / "GroupTheory", "Mathlib" / "RepresentationTheory", - "Mathlib" / "LinearAlgebra"] }, + "Mathlib" / "LinearAlgebras"] }, { label := "t-algebraic-geometry", dirs := #[ "Mathlib" / "AlgebraicGeometry",