8000 Warning "there are two interface files" should not be serialized · Issue #7104 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
Warning "there are two interface files" should not be serialized #7104
New issue
New issue
Closed
#7112
Closed
Warning "there are two interface files" should not be serialized#7104
#7112
Assignees
andreasabel
Labels
release blockerIssues blocking the next Agda releaseux: warningsIssues relating to the reporting of warnings
Milestone
 
2.6.4.2
@andreasabel

Description

@andreasabel
andreasabel
opened on Feb 11, 2024

The new warning "there are two interface files" should not be serialized, and it should be a named warning, not a GenericWarning.
This warning was introduced by:

Metadata

Metadata

Assignees

Labels

release blockerIssues blocking the next Agda releaseux: warningsIssues relating to the reporting of warnings

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions
    0