minor

.github/workflows/leaderboard.yml

@@ -72,14 +72,14 @@ jobs:
       - name: Add leaderboard entry
         run: PYTHONPATH=$PYTHONPATH:. uv run scripts/add_to_leaderboard.py --pr-branch ${{ steps.get-branch.outputs.branch }} ${{ env.experiment_prefixes }}
 
-      - name: Comment with leaderboard entry
+      - name: Comment on PR
         if: ${{ success() }}
         uses: actions/github-script@v6
         with:
           script: |
             const fs = require('fs');
             const content = fs.readFileSync('.temp/added_leaderboard_data.json', 'utf8');
-            const commentBody = `### Added leaderboard entry\n${content}`;
+            const commentBody = `### Added to leaderboard:\n${content}`;
             const issue_number = context.issue.number;
             await github.rest.issues.createComment({
               ...context.repo,
@@ -126,26 +126,20 @@ jobs:
       - name: Remove leaderboard entries
         run: PYTHONPATH=$PYTHONPATH:. uv run scripts/remove_from_leaderboard.py --save-removed --ids ${{ env.ids }}
 
-      - name: Reformat leaderboard in the original format
-        run: |
-          python - <<EOF
-          import json
-
-          with open("experiments/outputs/_leaderboard.json") as file:
-            data = json.load(file)
-
-          def normalize_numbers(obj):
-            if isinstance(obj, int):
-                return float(obj)
-            elif isinstance(obj, dict):
-                return {k: normalize_numbers(v) for k, v in obj.items()}
-            elif isinstance(obj, list):
-                return [normalize_numbers(v) for v in obj]
-            return obj
-
-          with open("experiments/outputs/_leaderboard.json", "w") as file:
-            json.dump(normalize_numbers(data), file, indent=4)
-          EOF
+      - name: Comment on PR
+        if: ${{ success() }}
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const fs = require('fs');
+            const content = fs.readFileSync('.temp/removed_leaderboard_data.json', 'utf8');
+            const commentBody = `### Removed from leaderboard:\n${content}`;
+            const issue_number = context.issue.number;
+            await github.rest.issues.createComment({
+              ...context.repo,
+              issue_number: issue_number,
+              body: commentBody,
+            });
 
       - name: Commit and push
         run: |