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

Clean up DOMJudgeService #2872

Merged
merged 7 commits into from
Dec 5, 2024
Merged

Clean up DOMJudgeService #2872

merged 7 commits into from
Dec 5, 2024

Conversation

eldering
Copy link
Member

@eldering eldering commented Dec 3, 2024

Remove a bunch of stuff that doesn't have to be here and that causes unnecessary dependencies.

And fix bug in getting verdicts as reported in slack.

@eldering eldering force-pushed the cleanup-dj-service branch 3 times, most recently from 50f854b to 61f48c7 Compare December 4, 2024 21:08
They don't depend on any DOMjudge internals.
Also add some documentation.
This was broken in 754779b.

As reported by Shengliang Cai and based on a patch by @Kevinjil.
Copy link
Member

@vmcj vmcj left a comment

Choose a reason for hiding this comment

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

The mistake was already in the original code but still good to keep it consistent.

webapp/src/Service/ConfigurationService.php Outdated Show resolved Hide resolved
webapp/src/Service/ConfigurationService.php Outdated Show resolved Hide resolved
Co-authored-by: MCJ Vasseur <14887731+vmcj@users.noreply.github.com>
@eldering eldering enabled auto-merge December 5, 2024 22:16
@eldering eldering added this pull request to the merge queue Dec 5, 2024
Merged via the queue into main with commit a3f6898 Dec 5, 2024
33 of 39 checks passed
@eldering eldering deleted the cleanup-dj-service branch December 5, 2024 22:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants