diff options
Diffstat (limited to 'clippy_dev/src')
| -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() |
