Wasmtime GitHub notifications bot (Mar 09 2022 at 21:17): Wasmtime GitHub notifications bot (Mar 09 2022 at 21:17):github-actions[bot] commented on issue #3909:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:x64", "isle", "wasmtime:docs"Thus the following users have been cc'd because of the following labels:
- cfallin: isle
- fitzgen: isle
To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.
Learn more.
</details>
Wasmtime GitHub notifications bot (Mar 09 2022 at 21:24):cfallin commented on issue #3909:
Hmm, so the option to merge this with two separate commits (the cherrypick of the earlier PR, and then the release-notes update) is disabled because the repository now only allows "Squash and Merge". This is probably not the right solution for merges into release branches that are actually carrying multiple logically separate changes around; if I had to cherrypick multiple PRs into the point release then it would seem wrong to squash them together; cc @tschneidereit to think more about this / perhaps see if we can have the restriction only on
main?In any case, for forward progress, I'll go ahead and merge this.
Last updated: Nov 22 2024 at 16:03 UTC