Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Agda Tests #3517

Merged
merged 2 commits into from
Nov 11, 2023
Merged

Add Agda Tests #3517

merged 2 commits into from
Nov 11, 2023

Conversation

rzuckerm
Copy link
Collaborator

@rzuckerm rzuckerm commented Nov 9, 2023

Congrats on taking the first step to contributing to the Sample Programs repository maintained by The Renegade Coder!
For simplicity, please make sure that your pull request includes one and only one contribution.

Please fill one of the sections below as applicable.
Please also add any other relevant information to the Notes section at the bottom.
You may delete or just ignore any other sections.
For more information please refer to our contributing documentation

I Am Adding New Tests for a Language

  • I fixed Add Agda Testing #3516
  • I named the pull request using Add {LANGUAGE} Tests format
  • I added a testinfo.yml files (see contributing documentation)
    • I used an officially supported docker image or one that I personally trust
  • I verified all tests are passing

Other Notes

I had to modify the "hello world" sample to get it to work.

@rzuckerm rzuckerm added enhancement Any code that improves the repo tests Testing related labels Nov 9, 2023
@rzuckerm rzuckerm marked this pull request as ready for review November 9, 2023 01:33
@jrg94 jrg94 requested a review from a team November 11, 2023 00:26
@jrg94 jrg94 self-assigned this Nov 11, 2023
Copy link
Member

@jrg94 jrg94 left a comment

Choose a reason for hiding this comment

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

Wow! Very strange looking language that requires many imports.

@jrg94 jrg94 merged commit c9a84e9 into TheRenegadeCoder:main Nov 11, 2023
6 checks passed
@rzuckerm rzuckerm deleted the add-agda-tests branch November 11, 2023 12:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Any code that improves the repo tests Testing related
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add Agda Testing
2 participants