Commit 2023-05-11 11:48 cc90075e
View on Github →chore: make sorry only a warning again in the editor (#3919)
Sorry everyone, my fault that sorry has been an error in the editor the past two weeks. I merged https://github.com/leanprover-community/mathlib4/pull/3556 prematurely.
This PR leaves sorry as an error during lake build (and when rebuilding dependencies in VSCode), but in your active editor it is only a warning.