clarified database update: full ml_statistics on server, no ml_statistics on plain file;
authorwenzelm
Sun, 30 Apr 2017 17:02:56 +0200
changeset 65647 7cf60e2b9115
parent 65646 014dbbe5331f
child 65648 69dfec14b0df
clarified database update: full ml_statistics on server, no ml_statistics on plain file;
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))
   }