feat: workflow to update and build #6
Conversation
|
I realise now that two changes that probably should be made:
|
|
|
||
| jobs: | ||
| update_lean: | ||
| update: |
There was a problem hiding this comment.
Run on main branch only.
| update: | |
| update: | |
| if: github.ref == 'refs/heads/main' |
.github/workflows/update.yaml
Outdated
| - name: Commit updated version | ||
| if: steps.update-lean-mathlib.outputs.result == 'update-success' | ||
| run: | | ||
| git config user.name "$GITHUB_ACTOR" |
There was a problem hiding this comment.
I want to use action@github.com for commiter. (same as build.yaml)
Co-authored-by: Kitamado <47292598+Seasawher@users.noreply.github.com>
|
Concerning the git user, after some reading it appears the best option is: git config user.name "github-actions[bot]"
git config user.email "41898282+github-actions[bot]@users.noreply.github.com"However any option still does the job in this particular use case. On the other hand, the commit step could be completely removed. It could be arranged in a way that the only thing done is that every day an updated version is deployed to pages. In this sense an updated version of the repo is not required. Let me know your preference and I can update the workflow correspondingly. My only objective was that the list of tactics on the page is always up to date with zero effort from humans. |
The commit step is necessary. The reason is that a markdown file is in this repository. I check the differences by looking at the markdown file. |
Thank you! However, for uniformity, please use the same commit method as in |
It seemed that it could be useful to have a custom workflow that can run everyday, check for updates and deploy the updated version directly. Here is a first attempt at such.
I have tested it a bit and seems fine although I haven't tested very extensively. Let me know if something like this is useful and if you have any requests for modifications, etc.