Skip to content

[Merged by Bors] - chore: fix #align lines#3640

Closed
Parcly-Taxel wants to merge 8 commits intomasterfrom
nna
Closed

[Merged by Bors] - chore: fix #align lines#3640
Parcly-Taxel wants to merge 8 commits intomasterfrom
nna

Conversation

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel commented Apr 25, 2023

This PR fixes two things:

  • Most align statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (s/\n\n#align/\n#align). This is often seen in the mathport output after ending calc blocks.
  • All remaining more-than-one-line #align statements. (This was needed for a script I wrote for [Merged by Bors] - fix: add missing _root_ #3630.)

Open in Gitpod

@Parcly-Taxel Parcly-Taxel changed the title chore: fix all chore: fix #align lines Apr 25, 2023
@Parcly-Taxel Parcly-Taxel added the WIP Work in progress label Apr 25, 2023
@Parcly-Taxel Parcly-Taxel added awaiting-review and removed WIP Work in progress labels Apr 25, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 25, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 25, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Apr 25, 2023

Already running a review

bors bot pushed a commit that referenced this pull request Apr 25, 2023
This PR fixes two things:
* Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks.
* **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
@bors
Copy link
Copy Markdown

bors bot commented Apr 25, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: fix #align lines [Merged by Bors] - chore: fix #align lines Apr 25, 2023
@bors bors bot closed this Apr 25, 2023
@bors bors bot deleted the nna branch April 25, 2023 14:46
kim-em pushed a commit that referenced this pull request May 10, 2023
This PR fixes two things:
* Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks.
* **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
This PR fixes two things:
* Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks.
* **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
This PR fixes two things:
* Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks.
* **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
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