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 /docs | |
| 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 'docs')
0 files changed, 0 insertions, 0 deletions