Merge develop into master (!1220) · Merge requests · Codalab / codabench · GitLab

Placeholder Adrien Pavão requested to merge develop into master Nov 10, 2023

We need to deploy this quickly because of this change:

#1218

Other change:

#1219