Merge develop into master#1040

Didayolo merged 3 commits into

mastercodalab/codabench:masterfrom

developcodalab/codabench:developCopy head branch name to clipboard