search

coq-community / docker-coq-action

GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
MIT License
12 stars 4 forks source link

New fine-grained customization does not allow groups within each section #34

Closed tchajed closed 4 years ago

tchajed commented 4 years ago

The new value for custom_script that includes all the sections surrounds each one with a startGroup with a generic name:

startGroup before_install dependencies
  {{before_install}}
endGroup
startGroup install dependencies
  {{install}}
endGroup
startGroup after_install dependencies
  {{after_install}}
endGroup
startGroup before_script
  {{before_script}}
endGroup
startGroup script
  {{script}}
endGroup
startGroup after_script
  {{after_script}}
endGroup
startGroup uninstall
  {{uninstall}}
endGroup

Those names are a bit annoying on their own, but worse GitHub actions doesn't seem to support nested groups so they forbid adding any user groups (unless you rewrite custom_script, of course).

erikmd commented 4 years ago

Hi @tchajed indeed, even if the startGroup / endGroup were not directly documented, they can be handy. And with the latest version of custom_script, this does not allow using one's own startGroup/endGroup in the install: script: new fields... I will quickly propose a PR.