Stream: coqbot devs & users

Topic: direct links


view this post on Zulip Gaëtan Gilbert (Sep 16 2022 at 12:44):

Didn't we use to have direct links to logs on gitlab instead of going through the github checks page?
ie https://gitlab.com/coq/coq/-/jobs/3034676107 instead of https://github.com/coq/coq/pull/16493/checks?check_run_id=8379143914

view this post on Zulip Théo Zimmermann (Sep 16 2022 at 13:00):

Hum, that was a very long time ago (before coqbot started to use the Checks tab in 2020), wasn't it?

view this post on Zulip Théo Zimmermann (Sep 16 2022 at 13:01):

Adding direct links without removing the Checks feature would unfortunately amount to duplicating every failed check.

view this post on Zulip Gaëtan Gilbert (Sep 16 2022 at 13:15):

Théo Zimmermann said:

Hum, that was a very long time ago (before coqbot started to use the Checks tab in 2020), wasn't it?

after using the checks tab the direct links were made to work again until recently
or maybe it's an extension I had that stopped working? not sure

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

or maybe it's an extension I had that stopped working? not sure

Probably, because I don't recall anything like this.

view this post on Zulip Ali Caglayan (Sep 17 2022 at 15:32):

I am using the refined github extension which makes the links direct. Occasionally it stops working and takes me to the checks tabs.


Last updated: Jan 31 2023 at 10:01 UTC