diff options
author | Daniel McNab <[email protected]> | 2021-03-06 13:56:42 +0000 |
---|---|---|
committer | Daniel McNab <[email protected]> | 2021-03-06 13:56:42 +0000 |
commit | 7513867aa21a638eac86c72c8eae0f9ba834380d (patch) | |
tree | adb1cb5206b471ca49d42af2a8e63e5c39d14f05 /.github/workflows/release.yaml | |
parent | 1076d21fc0d86ae3b7bb7fca610548fedd42ab4a (diff) |
If a manual dependency exists, don't overwrite
This is a hack to work around miri being included in
our analysis of rustc-dev
Really, we should probably use an include set of the actual root libraries
I'm not sure how those are determined however
Diffstat (limited to '.github/workflows/release.yaml')
0 files changed, 0 insertions, 0 deletions