Skip to content

chore: revert "add dev console logging (#784)" - #793

Merged
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-vpmvryrymnuy
Jul 29, 2026
Merged

chore: revert "add dev console logging (#784)"#793
mhuisi merged 1 commit into
leanprover:masterfrom
mhuisi:push-vpmvryrymnuy

Conversation

@mhuisi

@mhuisi mhuisi commented Jul 29, 2026

Copy link
Copy Markdown
Collaborator

Nobody ended up providing more information based on this debug logging, so we are removing this again for now.

@mhuisi mhuisi changed the title chore: revert add dev console logging (#784) chore: revert "add dev console logging (#784)" Jul 29, 2026
@mhuisi
mhuisi merged commit d08e333 into leanprover:master Jul 29, 2026
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant