Skip to content

fix-whitespace fixes#435

Merged
jespercockx merged 4 commits intoagda:masterfrom
liesnikov:master
Oct 8, 2025
Merged

fix-whitespace fixes#435
jespercockx merged 4 commits intoagda:masterfrom
liesnikov:master

Conversation

@liesnikov
Copy link
Contributor

Adding fix-whitespace to the nix devshell derivation and fixing the makefile

@jespercockx
Copy link
Member

Thank youuu!

@jespercockx jespercockx merged commit 13db471 into agda:master Oct 8, 2025
8 checks passed
@jespercockx jespercockx added this to the 1.5 milestone Oct 14, 2025
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