diff options
| author | Dylan DPC <dylan.dpc@gmail.com> | 2021-04-19 22:00:11 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-19 22:00:11 +0200 |
| commit | a23fd1694de044565890faa10125f451b454d67b (patch) | |
| tree | a365af72f7786a1e072ec2b58ad5a60abf43be12 /compiler/rustc_mir/src/transform/coverage/mod.rs | |
| parent | 349fae3a32cfcb650f252104bb5c88ee32d9bebf (diff) | |
| parent | 4fa1d6177cdb251254ecf37941fd2f7c73f2d6e0 (diff) | |
| download | rust-a23fd1694de044565890faa10125f451b454d67b.tar.gz rust-a23fd1694de044565890faa10125f451b454d67b.zip | |
Rollup merge of #84330 - GuillaumeGomez:remove-footer, r=jyn514
Remove unused footer section I realized yesterday while working on docs.rs that rustdoc was generating a "footer"section that it doesn't use. No need to keep it then. r? `@jyn514`
Diffstat (limited to 'compiler/rustc_mir/src/transform/coverage/mod.rs')
0 files changed, 0 insertions, 0 deletions