From e6292bc0b890aed51447c1f6ef1cd503bd3abf0f Mon Sep 17 00:00:00 2001
From: Denis Gorbachev <829578+DenisGorbachev@users.noreply.github.com>
Date: Sat, 30 Sep 2023 18:51:35 +0700
Subject: [PATCH] doc: fix docstring typos (#2605)

* lake: fix a typo in `get_config?` syntax doc
* fix a typo in `withImporting` doc
---
 src/Lean/ImportingFlag.lean   | 2 +-
 src/lake/Lake/DSL/Config.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean
index 2a43538dd9..16370c0f94 100644
--- a/src/Lean/ImportingFlag.lean
+++ b/src/Lean/ImportingFlag.lean
@@ -42,7 +42,7 @@ the `initialize` command to update global references.
 IMPORTANT: There is no semaphore controlling the access to these global references.
 We assume these global references are updated by a single execution thread.
 This is true in the Lean frontend where we process the `import` commands at the beginning
-of the execution only. Users must make sure that `importModules` is used, there is only
+of the execution only. Users must make sure that when `importModules` is used, there is only
 one execution thread accessing the global references.
 -/
 def withImporting (x : IO α) : IO α :=
diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean
index 05c09499ec..1ea682f2b7 100644
--- a/src/lake/Lake/DSL/Config.lean
+++ b/src/lake/Lake/DSL/Config.lean
@@ -40,7 +40,7 @@ def elabDirConst : TermElab := fun stx expectedType? => do
 
 /--
 A macro that expands to the specified configuration option (or `none`,
-if not the option has not been set) during the Lakefile's elaboration.
+if the option has not been set) during the Lakefile's elaboration.
 
 Configuration arguments are set either via the Lake CLI (by the `-K` option)
 or via the `with` clause in a `require` statement.