Showing content from https://github.com/agda/agda/issues/7912 below:
[ModuleNameDoesntMatchFileName] · Issue #7912 · agda/agda · GitHub
Skip to content Navigation Menu
Search code, repositories, users, issues, pull requests...
Saved searches Use saved searches to filter your results more quickly
Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
Missing error location for error: [ModuleNameDoesntMatchFileName] #7912
Assignees
Description
This is a problem for instance when batch-building with agda --build-library. Agda tells me where it expected this module to be, but not the path where this module actually resides.
Metadata Metadata
Development
No branches or pull requests Issue actions
You can’t perform that action at this time.
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4