# HG changeset patch
# User wenzelm
# Date 1493564576 -7200
# Node ID 7cf60e2b9115a07bfeb45fdc1d9ee3b553570471
# Parent  014dbbe5331f29952717d993dbec4bab37b08d9c
clarified database update: full ml_statistics on server, no ml_statistics on plain file;

diff -r 014dbbe5331f -r 7cf60e2b9115 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Apr 30 16:47:30 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Apr 30 17:02:56 2017 +0200
@@ -30,6 +30,8 @@
 
   val release_snapshot = Path.explode("~/html-data/release_snapshot")
 
+  val build_log_snapshot = Path.explode("~/html-data/build_log.db")
+
 
 
   /** particular tasks **/
@@ -150,8 +152,9 @@
   def database_update(options: Options)
   {
     val store = Build_Log.store(options)
-    using(store.open_database())(db =>
-      store.write_info(db, Build_Log.Log_File.find_files(database_dirs)))
+    val files = Build_Log.Log_File.find_files(database_dirs)
+    using(store.open_database())(db => store.write_info(db, files, ml_statistics = true))
+    using(SQLite.open_database(build_log_snapshot))(db => store.write_info(db, files))
   }