Skip to content

Do not treat default warnings as errors in dune#158

Open
andres-erbsen wants to merge 2 commits into
rocq-community:masterfrom
andres-erbsen:patch-2
Open

Do not treat default warnings as errors in dune#158
andres-erbsen wants to merge 2 commits into
rocq-community:masterfrom
andres-erbsen:patch-2

Conversation

@andres-erbsen

@andres-erbsen andres-erbsen commented Jun 4, 2025

Copy link
Copy Markdown
Contributor

#157 (comment)

Untested

Comment thread theories/dune Outdated
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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.

2 participants