Stream: MetaCoq

Topic: make all and translations


view this post on Zulip Gaëtan Gilbert (Dec 13 2023 at 11:51):

In Coq CI we don't check metacoq-translations because it's not in the all target https://github.com/MetaCoq/metacoq/blob/9b70a137ed8e0b00c7a3b76a44cac9ff738e8ab4/Makefile#L2
is there some reason for this?

view this post on Zulip Matthieu Sozeau (Dec 13 2023 at 12:57):

We can put it back in the all target


Last updated: Jul 23 2024 at 21:01 UTC