[Merged by Bors] - chore: avoid redundant error message in differential geometry elaborators#34527
[Merged by Bors] - chore: avoid redundant error message in differential geometry elaborators#34527grunweg wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
|
@adomani @Vierkantor This is a linter API question; perhaps you know a nice trick here. (Perhaps there already is some API for "check if this option is already enabled, and only add a hint about it if not enabled" that I can use.) |
PR summary 7cccd8a4caImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
This PR/issue depends on: |
cc6d67f to
754de07
Compare
|
I am not sure whether the issue is that you are using |
|
I guess my question was "is there an incantation which checks both options at once" --- given that these are tracing options, so |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Thanks for the quick review! |
|
Pull request successfully merged into master. Build succeeded: |
…tors (leanprover-community#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to leanprover-community#30744.
…tors (leanprover-community#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to leanprover-community#30744.
When a tracing option is already set, we don't need to tell the user about it. Follow-up to #30744.
My main question is if there's a better way to do this, e.g. doing only one check instead of two.