From 9d369e16aab6d6482b219cb3cae697c1058fb991 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Wed, 10 Dec 2025 19:51:56 -0800 Subject: [PATCH] chore: backtick identifiers in Lake eval messages --- src/lake/Lake/Load/Lean/Eval.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean index 02791dfa658a..8cc9d23f76e0 100644 --- a/src/lake/Lake/Load/Lean/Eval.lean +++ b/src/lake/Lake/Load/Lean/Eval.lean @@ -169,7 +169,7 @@ public def Package.loadFromEnv -- Deprecation warnings unless self.config.manifestFile.isNone do - logWarning s!"{self.prettyName}: package configuration option 'manifestFile' is deprecated" + logWarning s!"{self.prettyName}: package configuration option `manifestFile` is deprecated" -- Fill in the Package return {self with