Wasmtime GitHub notifications bot (Aug 08 2022 at 20:41): Wasmtime GitHub notifications bot (Aug 08 2022 at 20:41):github-actions[bot] commented on issue #4645:
Subscribe to Label Action
cc @cfallin, @fitzgen
<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:x64", "isle"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 (Aug 09 2022 at 16:52):elliottt commented on issue #4645:
This looks good to me as-is, but I'm curious to see if the rule-priority tweak we talked about today removes the need for the priority here before we merge it...
The bugfix you linked removes the need for the explicit priority here, so I'll make a separate PR for that before merging this without the priority :+1:
Last updated: Oct 23 2024 at 20:03 UTC