diff options
| author | flip1995 <philipp.krones@embecosm.com> | 2022-01-27 15:12:45 +0100 |
|---|---|---|
| committer | flip1995 <philipp.krones@embecosm.com> | 2022-01-27 15:12:45 +0100 |
| commit | cce9231c19378f57b05f3c8b09df317c3a512f82 (patch) | |
| tree | a99668f41abff07226f0f43c4555d1ccfea46804 /src/tools/clippy/util | |
| parent | 21b4a9cfdcbb1e76f4b36b5c3cfd64d627285093 (diff) | |
| parent | a98e7ab8b94485be6bd03e0c6b8682ecab5b52e6 (diff) | |
Merge commit 'a98e7ab8b94485be6bd03e0c6b8682ecab5b52e6' into clippyup
Diffstat (limited to 'src/tools/clippy/util')
| -rw-r--r-- | src/tools/clippy/util/gh-pages/index.html | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/tools/clippy/util/gh-pages/index.html b/src/tools/clippy/util/gh-pages/index.html index 5b7e61a349d..83a200ca3c4 100644 --- a/src/tools/clippy/util/gh-pages/index.html +++ b/src/tools/clippy/util/gh-pages/index.html @@ -522,6 +522,11 @@ Otherwise, have a great day =^.^= } scrollToLintByURL($scope); + + setTimeout(function () { + var el = document.getElementById('filter-input'); + if (el) { el.focus() } + }, 0); }) .error(function (data) { $scope.error = data; |