Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix docgram's dune file following #12085. #12994

Merged
merged 1 commit into from Sep 9, 2020

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Sep 8, 2020

Kind: infrastructure.

@Zimmi48 Zimmi48 added kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. labels Sep 8, 2020
@Zimmi48 Zimmi48 added this to the 8.12.1 milestone Sep 8, 2020
@Zimmi48 Zimmi48 requested a review from a team as a code owner September 8, 2020 15:25
@ejgallego ejgallego self-assigned this Sep 8, 2020
@ejgallego
Copy link
Member

Pretty strange failures, let's merge anyways as they do look unrelated.

@coqbot: merge now

p.s: I'm sure you already know @Zimmi48 but it'd be nice if we could restore the 1-click setting from details to gitlab's pipeline , if possible indeed now that coqbot is GH app.

@coqbot-app coqbot-app bot merged commit cdfe69d into coq:master Sep 9, 2020
@coqbot-app coqbot-app bot added this to Request 8.12.1 inclusion in Coq 8.12 Sep 9, 2020
@Zimmi48
Copy link
Member Author

Zimmi48 commented Sep 9, 2020

It's related to the use of the "Checks" API and tab rather than just the fact that coqbot is a GH app, although the latter was a prerequisite (cf. https://coq.zulipchat.com/#narrow/stream/243318-coqbot-devs.20.26.20users/topic/Checks). It's not something that we can control: the indirection is imposed by GitHub as we could see already from using Azure pipelines. However, by adding much more information to this Checks tab, I'm hoping to make it much more convenient and to reduce the need to follow the link to GitLab (another thing to do is to support restarting a failed job directly from GitHub, which would avoid requiring contributors to also register and request access on GitLab).

@ejgallego
Copy link
Member

Yeah, I read about the plan, which makes sense, but indeed the direct link was very convenient, users like me do really want to jump to gitlab. Github is becoming super clicky as of late.

@Zimmi48 Zimmi48 deleted the fix-docgram-dune branch September 9, 2020 15:37
Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 10, 2020
@coqbot-app coqbot-app bot moved this from Request 8.12.1 inclusion to Shipped in 8.12.1 in Coq 8.12 Sep 11, 2020
@coqbot-app coqbot-app bot moved this from Request 8.12.1 inclusion to Shipped in 8.12.1 in Coq 8.12 Sep 11, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools.
Projects
No open projects
Coq 8.12
  
Shipped in 8.12.1
Development

Successfully merging this pull request may close these issues.

None yet

2 participants