diff options
| -rw-r--r-- | clippy_dev/src/serve.rs | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/clippy_dev/src/serve.rs b/clippy_dev/src/serve.rs index d367fefec61..a2d1236629f 100644 --- a/clippy_dev/src/serve.rs +++ b/clippy_dev/src/serve.rs @@ -20,8 +20,14 @@ pub fn run(port: u16, lint: Option<String>) -> ! { loop { let index_time = mtime("util/gh-pages/index.html"); + let times = [ + "clippy_lints/src", + "util/gh-pages/index_template.html", + "tests/compile-test.rs", + ] + .map(mtime); - if index_time < mtime("clippy_lints/src") || index_time < mtime("util/gh-pages/index_template.html") { + if times.iter().any(|&time| index_time < time) { Command::new(env::var("CARGO").unwrap_or("cargo".into())) .arg("collect-metadata") .spawn() |