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

Move startGroup/endGroup constructs to individual fields #35

Merged
merged 3 commits into from
Nov 28, 2020
Merged

Conversation

erikmd
Copy link
Member

@erikmd erikmd commented Nov 27, 2020

Impact:

  • this slightly changes defaults values w.r.t. v1.2.0
  • but this is fully backward-compatible w.r.t. v1.1.0
  • and this makes it possible to customize group names (that cannot be nested)

I can readily do a point release if you want @tchajed ; otherwise tomorrow Saturday :)

@erikmd erikmd added the fix label Nov 27, 2020
@erikmd erikmd requested a review from tchajed November 27, 2020 21:39
Copy link
Member

@tchajed tchajed left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!

@tchajed
Copy link
Member

tchajed commented Nov 27, 2020

Up to you when to merge - I already effectively did this by overriding custom_script, once this is merged I can stop doing that.

@erikmd
Copy link
Member Author

erikmd commented Nov 27, 2020

BTW I've added some extra documentation on startGroup/endGroup (to document that they not only create foldable groups using the standard GHA feature, but also compute the intermediate elapsed time).

I'd like to merge this PR ASAP as it is a fix, however I'd be glad to have some review for the doc I have added (in a2a4cb7)

Cc @Zimmi48 FYI

@erikmd
Copy link
Member Author

erikmd commented Nov 27, 2020

In the meantime, note that even if this PR is not yet merged, the docker-coq-action can already be used as is by specifying the temporary branch fix-groups:

- uses: coq-community/docker-coq-action@fix-groups

@erikmd erikmd added the documentation Improvements or additions to documentation label Nov 27, 2020
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM but please fix the example overriding before_script, script and uninstall to create groups (in particular, this would replace the echo Workaround...).

Impact:
* this slightly changes defaults values w.r.t. v1.2.0
* but this is fully backward-compatible w.r.t. v1.1.0
* and this makes it possible to customize group names (that cannot be nested)
in order to be more robust and future-proof, if users happen to write
more involved group titles, involving special characters to be quoted.
@erikmd
Copy link
Member Author

erikmd commented Nov 28, 2020

Fixed, and will now release v1.2.1. Thanks @Zimmi48 for your review!

@erikmd erikmd merged commit 298d88f into master Nov 28, 2020
@erikmd erikmd deleted the fix-groups branch November 28, 2020 17:34
@erikmd
Copy link
Member Author

erikmd commented Nov 28, 2020

@tchajed

Up to you when to merge - I already effectively did this by overriding custom_script, once this is merged I can stop doing that.

Release done: https://github.com/coq-community/docker-coq-action/releases/tag/v1.2.1; so you'll be able to use the default custom_script from now on :)

@tchajed
Copy link
Member

tchajed commented Nov 28, 2020

Thanks @erikmd, I'm now taking advantage of this in Perennial.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation fix
Projects
None yet
Development

Successfully merging this pull request may close these issues.

New fine-grained customization does not allow groups within each section
3 participants