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

Estimated changes