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

[Merged by Bors] - correcting name of flag #2285

Closed
wants to merge 1 commit into from

Conversation

stefa2k
Copy link
Contributor

@stefa2k stefa2k commented Mar 26, 2021

Issue Addressed

None, just a very small fix of documentation

Proposed Changes

Fixing naming of paramter listed in documentation.

Additional Info

No changes to code, just fixing documentation

Copy link
Member

@paulhauner paulhauner left a comment

Choose a reason for hiding this comment

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

Thank you!!

bors r+

@paulhauner paulhauner added the ready-for-merge This PR is ready to merge. label Mar 29, 2021
bors bot pushed a commit that referenced this pull request Mar 29, 2021
## Issue Addressed

None, just a very small fix of documentation

## Proposed Changes

Fixing naming of paramter listed in documentation.

## Additional Info

No changes to code, just fixing documentation
@bors bors bot changed the title correcting name of flag [Merged by Bors] - correcting name of flag Mar 29, 2021
@bors bors bot closed this Mar 29, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-for-merge This PR is ready to merge.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants