Skip to content

[Merged by Bors] - chore: remove some double spaces#7983

Closed
mo271 wants to merge 2 commits intomasterfrom
mo271/double_spaces
Closed

[Merged by Bors] - chore: remove some double spaces#7983
mo271 wants to merge 2 commits intomasterfrom
mo271/double_spaces

Conversation

@mo271
Copy link
Copy Markdown
Collaborator

@mo271 mo271 commented Oct 27, 2023


Open in Gitpod

@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Oct 27, 2023

There many occurrences of two spaces after a period, entire sections are written in this style. I'm not sure if we want to make that more consistent, \. [A-Z] (with 2 spaces) has 523 matches, while \. [A-Z] (with 1 space) has 16529 matches, so clearly this is more common.

@alexjbest
Copy link
Copy Markdown
Member

Is this awaiting-review?

@mo271 mo271 added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Oct 28, 2023
@mo271
Copy link
Copy Markdown
Collaborator Author

mo271 commented Oct 28, 2023

Yes! awaiting review now; I added a few more.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 28, 2023
@sgouezel
Copy link
Copy Markdown
Contributor

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Oct 30, 2023
bors bot pushed a commit that referenced this pull request Oct 30, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link
Copy Markdown

bors bot commented Oct 30, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: remove some double spaces [Merged by Bors] - chore: remove some double spaces Oct 30, 2023
@bors bors bot closed this Oct 30, 2023
@bors bors bot deleted the mo271/double_spaces branch October 30, 2023 16:18
grunweg pushed a commit that referenced this pull request Nov 1, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
fgdorais pushed a commit that referenced this pull request Nov 1, 2023
Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants