Karl Palmskog (Sep 20 2022 at 15:19): Karl Palmskog (Sep 20 2022 at 15:19):Just a general comment, I think these kinds of error messages are terrible:
Error: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. [...]
I understand that the warning was changed into an error, but can't we have error messages sounding like actual errors? Just something like:
Error: Missing locality declaration
Karl Palmskog (Sep 20 2022 at 15:21):prompted by: https://github.com/coq/opam-coq-archive/pull/2316
Last updated: Dec 07 2023 at 14:02 UTC