Stream: git-wasmtime

Topic: wasmtime / PR #3423 Remove a dead script in the CI directory


view this post on Zulip Wasmtime GitHub notifications bot (Oct 07 2021 at 14:52):

alexcrichton opened PR #3423 from rm-dead-script to main:

This is no longer used on CI

<!--

Please ensure that the following steps are all taken care of before submitting
the PR.

Please ensure all communication adheres to the code of conduct.
-->

view this post on Zulip Wasmtime GitHub notifications bot (Oct 07 2021 at 15:17):

sunfishcode submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Oct 07 2021 at 15:57):

alexcrichton merged PR #3423.


Last updated: Dec 23 2024 at 13:07 UTC