Def RadarAPI.getRunInfo

Modification history

2026-01-30 13:30
LongestPole/Main.lean
chore: remove LongestPole (#34354) …
Deleted RadarAPI.getRunInfoView on Github →
2025-12-02 19:39
LongestPole/Main.lean
ci: decommission speedcenter (#32358) …
Added RadarAPI.getRunInfoView on Github →