print timing details (-d) in -q mode

diff --git a/kernel/driver.cc b/kernel/driver.cc
index cdf78460251aa830a11433bdd7ae95dac2d6dc13..b7cb414cee3a2f276606c6c9ce58f12225bf697a 100644 (file)
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -334,6 +334,10 @@ int main(int argc, char **argv)
                log_hasher = nullptr;
 
                log_spacer();
+
+               if (log_errfile != NULL && timing_details)
+                       log_files.push_back(stderr);
+
 #ifdef _WIN32
                log("End of script. Logfile hash: %s\n", hash.c_str());
 #else