Skip to content

Conversation

@zeme-wana
Copy link
Collaborator

This removes the warnings:

getExe: Package agda does not have the meta.mainProgram attribute. We'll assume that the main program has the same name for now, but this behavior is deprecated, because it leads to surprising errors when the assumption does not hold. If the package has a main program, please set `meta.mainProgram` in its definition to make this warning go away. Otherwise, if the package does not have a main program, or if you don't control its definition, use getExe' to specify the name to the program, such as lib.getExe' foo "bar".

@zeme-wana zeme-wana added the No Changelog Required Add this to skip the Changelog Check label Nov 3, 2025
@zeme-wana zeme-wana merged commit 704692a into master Nov 5, 2025
21 of 30 checks passed
@zeme-wana zeme-wana deleted the fix-agda-warning branch November 5, 2025 14:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

No Changelog Required Add this to skip the Changelog Check

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants