Merge develop into master - Quick fix#869

Didayolo merged 4 commits into

mastercodalab/codabench:masterfrom

developcodalab/codabench:developCopy head branch name to clipboard