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 →