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

Sharpen doc for min/max _ind functions #479

Merged
merged 1 commit into from
Jun 1, 2024
Merged

Conversation

jo-37
Copy link
Contributor

@jo-37 jo-37 commented Jun 1, 2024

No description provided.

@coveralls
Copy link

Coverage Status

coverage: 32.752% (-0.008%) from 32.76%
when pulling 07c3431 on jo-37:contrib
into a8400e6 on PDLPorters:master.

@mohawk2
Copy link
Member

mohawk2 commented Jun 1, 2024

Please don't create multiple PRs for one change. You could just have force-pushed your contrib branch rather than close and open a new one.

@mohawk2
Copy link
Member

mohawk2 commented Jun 1, 2024

Thanks for these!

@mohawk2 mohawk2 merged commit 87b795b into PDLPorters:master Jun 1, 2024
68 of 70 checks passed
@jo-37
Copy link
Contributor Author

jo-37 commented Jun 1, 2024

Please don't create multiple PRs for one change. You could just have force-pushed your contrib branch rather than close and open a new one.

Sorry, I don't understand. I accidentally pushed to a branch that was not completely merged. To avoid a total mess, I closed the PR and opened a new one. Though I'm not a complete git noob, I don't know how I could have done better.

@mohawk2
Copy link
Member

mohawk2 commented Jun 2, 2024

Pushing to a branch doesn't create a PR. A preferred option would have been to leave it open but mark it as "draft" (there's a button).

@jo-37
Copy link
Contributor Author

jo-37 commented Jun 2, 2024 via email

@mohawk2
Copy link
Member

mohawk2 commented Jun 2, 2024

Yes, I can see that you don't. The next time you open a PR by accident, please don't immediately close it, instead ask for advice. It is untidy and unnecessary to fire through more than one PR per intended change, and it's fine to just mark one as draft (so it can't be merged) if more needs doing.

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.

3 participants