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 option to change default judge of repository #3211

Closed
BTWS2 opened this issue Nov 15, 2021 · 1 comment
Closed

Add option to change default judge of repository #3211

BTWS2 opened this issue Nov 15, 2021 · 1 comment
Labels
feature New feature or request

Comments

@BTWS2
Copy link
Contributor

BTWS2 commented Nov 15, 2021

The default judge is used when the exercise doesn't specify one. The user can't change the default judge after the repository is added.

image
@BTWS2 BTWS2 added the feature New feature or request label Nov 15, 2021
@chvp chvp changed the title Add option to change default repository Add option to change default judge of repository Nov 16, 2021
@bmesuere bmesuere added this to Roadmap Apr 17, 2022
@bmesuere bmesuere moved this to Todo in Roadmap Apr 17, 2022
@bmesuere bmesuere moved this from Todo to Unplanned in Roadmap Apr 17, 2022
@BTWS2
Copy link
Contributor Author

BTWS2 commented Feb 9, 2023

Solved by #4381.

@BTWS2 BTWS2 closed this as completed Feb 9, 2023
@github-project-automation github-project-automation bot moved this from Unplanned to Done in Roadmap Feb 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature New feature or request
Projects
Roadmap
Status: Done
Milestone
No milestone
Development

No branches or pull requests
1 participant
@BTWS2