diff options
| author | Guillaume Gomez <guillaume1.gomez@gmail.com> | 2024-08-12 20:39:25 +0200 |
|---|---|---|
| committer | Guillaume Gomez <guillaume1.gomez@gmail.com> | 2024-09-22 22:30:44 +0200 |
| commit | b522e7a944341d463bf9091bd72faffcc807d875 (patch) | |
| tree | e6573de0fb3d8c6b4d93bfd5d4d88990256e6efd /clippy_dev/src | |
| parent | 43e338458168db91b8459735ba6ac0f230d78d92 (diff) | |
| download | rust-b522e7a944341d463bf9091bd72faffcc807d875.tar.gz rust-b522e7a944341d463bf9091bd72faffcc807d875.zip | |
Generate lint list in HTML directly instead of JS
Diffstat (limited to 'clippy_dev/src')
| -rw-r--r-- | clippy_dev/src/serve.rs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/clippy_dev/src/serve.rs b/clippy_dev/src/serve.rs index cc14cd8dae6..0216d884e2d 100644 --- a/clippy_dev/src/serve.rs +++ b/clippy_dev/src/serve.rs @@ -19,7 +19,7 @@ pub fn run(port: u16, lint: Option<String>) -> ! { }); loop { - if mtime("util/gh-pages/lints.json") < mtime("clippy_lints/src") { + if mtime("util/gh-pages/index.html") < mtime("clippy_lints/src") { Command::new(env::var("CARGO").unwrap_or("cargo".into())) .arg("collect-metadata") .spawn() |