Skip to content

Commit

Permalink
Do not put Everything.agda in the repo.
Browse files Browse the repository at this point in the history
  • Loading branch information
@JacquesCarette
JacquesCarette committed Apr 15, 2022
1 parent 4e5e7bb commit 8643687
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 411 deletions.
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
*.agdai
.DS_Store
src/MAlonzo
Everything.agda
Loading

5 comments on commit 8643687

@ncfavier
Copy link
Member

@ncfavier ncfavier commented on 8643687 Apr 17, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

Out of curiosity, why not? This file is used e.g. in the default build phase in Nixpkgs.

@ncfavier
Copy link
Member

Choose a reason for hiding this comment

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

Never mind, found the original issue.

@JacquesCarette
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Does this cause real problems for nix?

@ncfavier
Copy link
Member

Choose a reason for hiding this comment

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

No, we can just run make Everything.agda beforehand (or replace the build phase with make test). (cc actual maintainers @alexarice @turion)

@turion
Copy link
Contributor

@turion turion commented on 8643687 Apr 19, 2022

Choose a reason for hiding this comment

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

It doesn't cause real problems, but it's some extra effort.

Please sign in to comment.