Skip to content

Minor fixes from (#212)#2

Merged
jmacd merged 1 commit into
mainfrom
jmacd/onepr
Aug 10, 2023
Merged

Minor fixes from (#212)#2
jmacd merged 1 commit into
mainfrom
jmacd/onepr

Conversation

@jmacd
Copy link
Copy Markdown
Contributor

@jmacd jmacd commented Aug 10, 2023

Hypothesis: Creating this PR will result in EasyCLA running which will allow me to push -f the branch.
(This from #1, where the same happened.)

* Feedback from the PR #203

* typo
@jmacd jmacd merged commit 67d670e into main Aug 10, 2023
@jmacd
Copy link
Copy Markdown
Contributor Author

jmacd commented Aug 10, 2023

Hypothesis confirmed. If you push to the branch that the PR is requested against such that there's no diff, the PR somehow auto-merges. I didn't press any merge buttons on this PR, just pushed the commit to main.

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.

1 participant