diff options
| author | bors <bors@rust-lang.org> | 2024-10-11 14:18:54 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-10-11 14:18:54 +0000 |
| commit | 6f1def79dd372e380357e1dfd2b8a54254ffe2d0 (patch) | |
| tree | 8056cae564346d262ff72f3bc58f209b7aadf684 /clippy_dev | |
| parent | 8125cd5c2af8f609577c7d3b740a859fdde40c6c (diff) | |
| parent | 603934336dea3c8385f0c7a03ebf2ecebfe913a2 (diff) | |
| download | rust-6f1def79dd372e380357e1dfd2b8a54254ffe2d0.tar.gz rust-6f1def79dd372e380357e1dfd2b8a54254ffe2d0.zip | |
Auto merge of #13269 - GuillaumeGomez:rewrite-lints-page, r=Alexendoo
Rewrite lints page This PR has multiple goals: * Make lints page to work without needing a web server by removing the json file. * Prepare the field to also make the page work with JS (not done in this PR but should be straightforward). * Remove angular dependency. r? `@Alexendoo` changelog: make lint page work without web server
Diffstat (limited to 'clippy_dev')
| -rw-r--r-- | clippy_dev/src/serve.rs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/clippy_dev/src/serve.rs b/clippy_dev/src/serve.rs index cc14cd8dae6..d367fefec61 100644 --- a/clippy_dev/src/serve.rs +++ b/clippy_dev/src/serve.rs @@ -19,7 +19,9 @@ pub fn run(port: u16, lint: Option<String>) -> ! { }); loop { - if mtime("util/gh-pages/lints.json") < mtime("clippy_lints/src") { + let index_time = mtime("util/gh-pages/index.html"); + + if index_time < mtime("clippy_lints/src") || index_time < mtime("util/gh-pages/index_template.html") { Command::new(env::var("CARGO").unwrap_or("cargo".into())) .arg("collect-metadata") .spawn() |