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.

Sign up for GitHub

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

Jump to bottom

Add check that all tests are mentionned in tests/main #326

Merged
merged 1 commit into from
Apr 7, 2024
Merged

Add check that all tests are mentionned in tests/main #326

merged 1 commit into from
Apr 7, 2024

Conversation

GuillaumeGen
Copy link
Contributor

As suggested by @francoisthire in #325

@GuillaumeGen GuillaumeGen force-pushed the gg_check_tests branch 2 times, most recently from 8dd8fd1 to 320d30b Compare March 1, 2024 23:11
@GuillaumeGen
Copy link
Contributor Author

#327 was opened to illustrate that when a file is not mentioned in the main.ml file, then continuous integration fails and mentions the missing test.

@gabrielhdt gabrielhdt merged commit e0dd23c into Deducteam:master Apr 7, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gabrielhdt gabrielhdt gabrielhdt approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@GuillaumeGen @gabrielhdt