From 24cfae2421fee24988dc50e39caae7f86ffcb248 Mon Sep 17 00:00:00 2001 From: Connor Baker Date: Mon, 21 Aug 2023 01:08:44 -0400 Subject: [PATCH] doc: fix typo in Lake's Require DSL --- src/lake/Lake/DSL/Require.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean index e96824803e..c4a6921566 100644 --- a/src/lake/Lake/DSL/Require.lean +++ b/src/lake/Lake/DSL/Require.lean @@ -38,7 +38,7 @@ def expandDepSpec : TSyntax ``depSpec → MacroM Command | _ => Macro.throwUnsupported /-- -Adds a mew package dependency to the workspace. Has two forms: +Adds a new package dependency to the workspace. Has two forms: ```lean require foo from "path"/"to"/"local"/"package" with NameMap.empty