Def BenchAction.addBenchSummaryComment

Modification history

2025-12-02 19:39
scripts/bench_summary.lean
ci: decommission speedcenter (#32358) …
Deleted BenchAction.addBenchSummaryCommentView on Github →
2025-01-07 21:11
scripts/bench_summary.lean
fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) …
Modified BenchAction.addBenchSummaryCommentView on Github →
2024-11-25 06:35
scripts/bench_summary.lean
feat(bench_summary): report no significant changes and job_id (#18812) …
Modified BenchAction.addBenchSummaryCommentView on Github →
2024-11-07 21:30
scripts/bench_summary.lean
fix: percentages in bench report (#18732) …
Modified BenchAction.addBenchSummaryCommentView on Github →
2024-10-23 02:43
scripts/bench_summary.lean
feat(CI): add summary of benchmarking output (#16488) …
Added BenchAction.addBenchSummaryCommentView on Github →