search

leanprover / lean-action

GitHub action for standard CI in Lean projects
Apache License 2.0
16 stars 3 forks source link

fix: only end log group if lake command succeeds #94

Closed austinletson closed 3 months ago

austinletson commented 3 months ago

Ending the log group when a lake command fails prevented the log group from expanding on a command failure.

Related to #92