Skip to content

Port PR #28#1

Closed
MilesCranmer wants to merge 1 commit intomasterfrom
wendajiang/master
Closed

Port PR #28#1
MilesCranmer wants to merge 1 commit intomasterfrom
wendajiang/master

Conversation

@MilesCranmer
Copy link
Copy Markdown
Owner

Merging downstream PR nivekuil#28.

I think some of it conflicts with existing changes but just want to make the PR to track things.

@MilesCranmer
Copy link
Copy Markdown
Owner Author

Oh yeah this one looks like just formatting so I'll close it.

@MilesCranmer MilesCranmer deleted the wendajiang/master branch April 7, 2024 05:02
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