TODO: gr.DataFrame instead of Markdown table

app.py

@@ -147,7 +147,10 @@ def change_leaderboard_category(category):
     if category == leaderboard_server.TASKS_CATEGORY_OVERALL:
         task_abbreviation_legend = ""
     else:
+        # TODO: gr.DataFrame
         task_abbreviation_legend_head = [
+            "### Legend",
+            "",
             "| task abbreviation | task name |",
             "| --- | --- |",
         ]