Skip to content

Conversation

tisonkun
Copy link
Member

For #1079.

We can toggle the config once that PR gets merged.

For #1079.

We can toggle the config once that PR gets merged.
@merlimat merlimat merged commit c49345c into master Aug 15, 2023
@tisonkun tisonkun deleted the tisonkun-patch-1 branch August 15, 2023 23:44
tisonkun added a commit that referenced this pull request Aug 16, 2023
tisonkun added a commit that referenced this pull request Aug 16, 2023
Reverts #1080

The repo merge has been done. Regular PRs should go with squash and merge.
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.

2 participants