Skip to content

Add Agda CI script#557

Open
MatthewDaggitt wants to merge 3 commits intodevfrom
agda-ci
Open

Add Agda CI script#557
MatthewDaggitt wants to merge 3 commits intodevfrom
agda-ci

Conversation

@MatthewDaggitt
Copy link
Collaborator

No description provided.

@MatthewDaggitt MatthewDaggitt added enhancement New feature or request CI Continuous integration labels May 30, 2023
@MatthewDaggitt MatthewDaggitt changed the title Added CI script Add Agda CI script May 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Continuous integration enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants