Skip to content

Update Agda.gitignore to exclude MAlonzo directories in any location#4818

Merged
dooleydevin merged 1 commit intogithub:mainfrom
vicgeentor:patch-1
Apr 3, 2026
Merged

Update Agda.gitignore to exclude MAlonzo directories in any location#4818
dooleydevin merged 1 commit intogithub:mainfrom
vicgeentor:patch-1

Conversation

@vicgeentor
Copy link
Copy Markdown
Contributor

Reasons for making this change

When having multiple Agda projects in one repo, this will make sure that any MAlonzo directory will be ignored by git.

Links to documentation supporting these rule changes

https://wiki.portal.chalmers.se/agda/Docs/MAlonzo

Merge and Approval Steps

  • Confirm that you've read the contribution guidelines and ensured your PR aligns
  • Ensure CI is passing
  • Get a review and Approval from one of the maintainers

@vicgeentor vicgeentor requested a review from a team as a code owner March 18, 2026 13:10
@vicgeentor vicgeentor changed the title Agda.gitignore: include MAlonzo directories in any location Update Agda.gitignore to include MAlonzo directories in any location Mar 18, 2026
@vicgeentor vicgeentor changed the title Update Agda.gitignore to include MAlonzo directories in any location Update Agda.gitignore to exclude MAlonzo directories in any location Mar 18, 2026
Copy link
Copy Markdown
Collaborator

@dooleydevin dooleydevin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the contribution!

@dooleydevin dooleydevin merged commit f963896 into github:main Apr 3, 2026
@vicgeentor vicgeentor deleted the patch-1 branch April 4, 2026 04:26
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.

3 participants