diff options
| author | Matthias Krüger <matthias.krueger@famsik.de> | 2022-05-15 08:10:42 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-05-15 08:10:42 +0200 |
| commit | 7bf43c3931cbdde2f2d5bfe3456abde92ea1aa21 (patch) | |
| tree | 29e13f392baeb1866fb8a422f002631dbe4e09c0 /compiler/rustc_mir_transform/src/coverage/counters.rs | |
| parent | 7fb2d0ecef572120c4f2fc9a12a23f9bc9ace3d9 (diff) | |
| parent | dee294759ba141889f40689eda7345e89fe2bae5 (diff) | |
| download | rust-7bf43c3931cbdde2f2d5bfe3456abde92ea1aa21.tar.gz rust-7bf43c3931cbdde2f2d5bfe3456abde92ea1aa21.zip | |
Rollup merge of #96958 - GuillaumeGomez:settings-menu-display, r=jsha
Improve settings menu display and remove theme menu We talked about improving the settings menu and we mentioned that firefox pocket was a nice inspiration so I implemented it. The result looks like this:  You can test it [here](https://rustdoc.crud.net/imperio/settings-menu-display/doc/foo/index.html). Only question I have is: should I re-assign the shortcut `T` to this setting menu now that the theme menu is gone? For now I simply removed it. Important to be noted: the full settings page (at `settings.html`) is still rendered the same as currently. r? ``@jsha``
Diffstat (limited to 'compiler/rustc_mir_transform/src/coverage/counters.rs')
0 files changed, 0 insertions, 0 deletions