> @driazati notes that GitHub [just > introduced](https://github.blog/changelog/2022-08-23-new-options-for-controlling-the-default-commit-message-when-merging-a-pull-request/) > new options for controlling the default commit messages, so hopefully we can > leverage that to implement the merge and complement that with a lint tool.
This setting looks like it includes `@` tags from PRs in the default commit message which may make it a non-starter for us since that generates a lot of notifications -- Reply to this email directly or view it on GitHub: https://github.com/apache/tvm-rfcs/pull/88#issuecomment-1226673013 You are receiving this because you are subscribed to this thread. Message ID: <apache/tvm-rfcs/pull/88/c1226673...@github.com>
