Gaëtan Gilbert (Sep 16 2022 at 12:44): 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
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?
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.
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
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.
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: Dec 07 2023 at 14:02 UTC