Formed in 2009, the Archive Team (not to be confused with the archive.org Archive-It Team) is a rogue archivist collective dedicated to saving copies of rapidly dying or deleted websites for the sake of history and digital heritage. The group is 100% composed of volunteers and interested parties, and has expanded into a large amount of related projects for saving online and digital history.
Add MAlonzo directory. #2978
Merged
Add MAlonzo directory. #2978
Conversation
|
@mcoblenz thanks! |
Kiku-Reise
added a commit
to Kiku-Reise/gitignore
that referenced
this pull request
Apr 6, 2019
Ortega-Dan
added a commit
to Ortega-Dan/gitignore
that referenced
this pull request
Jun 26, 2019
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Reasons for making this change:
Agda generates a MAlonzo directory, which should not be included in repositories.
Links to documentation supporting these rule changes:
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo