summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorNadrieril2024-04-22 13:50:09 +0200
committerNadrieril2024-04-22 13:58:11 +0200
commite79e1d1aba6f6e2ff2517cd12b464f15899926da (patch)
treefa537e93d03a5bfbbdf0e6595fa7deaef53b8730 /backends/lean/Base
parent1e2fce0e1fa42fa2ba5800332e1fdfcba2294657 (diff)
ci: avoid running duplicate jobs
Diffstat (limited to 'backends/lean/Base')
0 files changed, 0 insertions, 0 deletions