Skip to content

Improve the list of files that git ignores#484

Merged
JacquesCarette merged 1 commit intoagda:masterfrom
tillrampe:gitignore
Aug 3, 2025
Merged

Improve the list of files that git ignores#484
JacquesCarette merged 1 commit intoagda:masterfrom
tillrampe:gitignore

Conversation

@tillrampe
Copy link
Contributor

No description provided.

@JacquesCarette JacquesCarette merged commit 4f4d14e into agda:master Aug 3, 2025
1 check passed
@tillrampe tillrampe mentioned this pull request Jan 13, 2026
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