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

chore: Set Git identity for gh-pages commits #198

Merged
merged 1 commit into from
Dec 12, 2023

Conversation

nojaf
Copy link
Collaborator

@nojaf nojaf commented Dec 12, 2023

The git identity needs to be set in https://github.com/fsprojects/Argu/actions/runs/7181861887/job/19557118490

Because a commit is being pushed to the gh-pages branch.

@nojaf nojaf requested a review from bartelink December 12, 2023 13:18
Copy link
Member

@bartelink bartelink left a comment

Choose a reason for hiding this comment

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

LGTM
no need to request reviews esp for things like this, unless you feel the need to...
you are the primary maintainer after all!

@bartelink bartelink changed the title Set Git identity. chore: Set Git identity for gh-pages commits Dec 12, 2023
@bartelink
Copy link
Member

@nojaf nojaf merged commit 3c8c539 into fsprojects:master Dec 12, 2023
4 checks passed
@nojaf
Copy link
Collaborator Author

nojaf commented Dec 12, 2023

Thanks!

aside: fsprojects/fsharp-cheatsheet#20 (comment)

I can't say I care enough for this project to start doing this. I don't do this anywhere and life goes on. I don't mind if you can't help yourself and want to change the titles. But I'm not sure if I see myself doing this. Changes might increase if a tl;dr of this was listed in the PR template.
Hope I'm not coming off as rude, just being upfront about my thoughts.

@bartelink
Copy link
Member

Yes, that's perfectly reasonable; appreciate the frankness
(But you will look back on this as a "wow it took me a while to get into it at the start!" thing some day :D)

The sell for me is that it feels like it helps me formulate shorter but more informative PR titles...

bartelink pushed a commit to bartelink/Argu that referenced this pull request Feb 19, 2024
bartelink pushed a commit to bartelink/Argu that referenced this pull request Feb 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants