Added category "Overall with details" to dropdown menu

app.py

@@ -576,7 +576,12 @@ def gradio_app():
 
                     with gr.Row():
                         leaderboard_category_of_tasks = gr.Dropdown(
-                            choices=[leaderboard_server.TASKS_CATEGORY_OVERALL] + sorted(leaderboard_server.TASKS_CATEGORIES),
+                            choices=(
+                                [
+                                    leaderboard_server.TASKS_CATEGORY_OVERALL,
+                                    leaderboard_server.TASKS_CATEGORY_OVERALL_DETAILS,
+                                ] + sorted(leaderboard_server.TASKS_CATEGORIES)
+                            ),
                             value=leaderboard_server.TASKS_CATEGORY_OVERALL,
                             label="Category of benchmarks",
                             interactive=True,
@@ -700,7 +705,11 @@ def gradio_app():
                 
                 with gr.Row():
                     model_details_category_of_tasks = gr.Dropdown(
-                        choices=sorted(leaderboard_server.TASKS_CATEGORIES),
+                        choices=(
+                            [
+                                leaderboard_server.TASKS_CATEGORY_OVERALL,
+                            ] + sorted(leaderboard_server.TASKS_CATEGORIES)
+                        ),
                         value=None,
                         label="Category of benchmarks",
                         visible=False,