I've requested that `lean-action` support this out of the box: [#general > lean-action @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/lean-action/near/531954797). Hopefully we can use that, but otherwise we should set it up manually.