Commit 2023-10-20 16:10 b8e9a283
View on Github →fix(says tactic): Don’t stumble over Try this:\n
instead of Try this:␣
(#7803)
as discussed in
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Lake.20build.20succeeds.20on.20local.2C.20but.20fails.20on.20GitHub.20Action/near/397679705