Stream: Hydras & Co. universe

Topic: Badges


view this post on Zulip Théo Zimmermann (Sep 14 2022 at 15:28):

We could update the "chat" value of the meta.yml files of related repositories and regenerate READMEs so that they point here.

view this post on Zulip Karl Palmskog (Sep 14 2022 at 15:29):

Sounds good to me, I think some project already does this?

view this post on Zulip Théo Zimmermann (Sep 14 2022 at 15:37):

Yes, several outside Coq-community, and graph-theory inside. But I realize by looking at their README that the feature was not really planned for Coq-community users. It would be better that the chat link replaces the one that is already provided (without changing its color) instead of adding a new one, wouldn't it?

view this post on Zulip Karl Palmskog (Sep 14 2022 at 15:38):

sure, yes, we just allow overriding the default link and keep everything as-is?

view this post on Zulip Théo Zimmermann (Sep 14 2022 at 15:40):

Either this, or we do this only in case a project has coq-community: true set.

view this post on Zulip Karl Palmskog (Sep 14 2022 at 19:28):

OK, I'd propose add configurability of chat link only for the case when community: true (postpone the general problem)

view this post on Zulip Théo Zimmermann (Sep 15 2022 at 08:35):

the chat: variable is already supported and already does something, so do you mean using a different variable when community: true? My idea was to just treat this chat: value differently depending on whether community: true or not.

view this post on Zulip Karl Palmskog (Sep 15 2022 at 08:39):

wait, so if both chat and community is defined, we only show the chat one?

view this post on Zulip Théo Zimmermann (Sep 15 2022 at 08:44):

No, what I had in mind was: we only show the community one but we change the URL using the chat.url value (this assumes that it will anyway always be a Zulip chat and that we do not want to change the shield text, though actually we could use chat.shield to make it possible to change the shield text).


Last updated: Apr 20 2024 at 12:02 UTC