rank leaderboard by mean task rank (MTR) instead of average across datasets. add 'export to json' button to make it easier for people to access the underlying leaderboard data.
42706ac
k8si
commited on