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

Run all tests with double translation too #1821

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Run all tests with double translation too #1821

wants to merge 8 commits into from
+29 −136

Conversation

OlivierNicole
Copy link
Contributor

This requires some care to avoid Dune setting the flag --effects= twice.

@OlivierNicole OlivierNicole mentioned this pull request Jan 28, 2025
Merged
@OlivierNicole @vouillon
CR
268cdb3 
Co-authored-by: Jérôme Vouillon <[email protected]>
@vouillon vouillon force-pushed the more-tests-double-translation branch 4 times, most recently from beaea9a to 4bfe5b9 Compare January 29, 2025 14:46
@vouillon vouillon force-pushed the more-tests-double-translation branch from 73fa4f8 to e9e9feb Compare January 29, 2025 15:51
@OlivierNicole
Copy link
Contributor Author

@vouillon It looks like you have erased some of my commits when force-pushing. I’ll re-add them on top when the CI has finished.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@vouillon vouillon vouillon approved these changes

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

Successfully merging this pull request may close these issues.
2 participants
@OlivierNicole @vouillon