# HG changeset patch
# User wenzelm
# Date 1493456197 -7200
# Node ID 218dbe4fb484a5326fbf0364498b8d744061f134
# Parent  ee917f172912efb8f06cc61f6d2b3832e5026a42
tuned signature;

diff -r ee917f172912 -r 218dbe4fb484 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Apr 29 10:53:02 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Apr 29 10:56:37 2017 +0200
@@ -651,6 +651,12 @@
           else Some(SSH.init_context(options).open_session(ssh_host, ssh_user, port)))
     }
 
+    def write_info(db: SQL.Database, files: List[JFile])
+    {
+      write_meta_info(db, files)
+      write_build_info(db, files)
+    }
+
     def filter_files(db: SQL.Database, table: SQL.Table, files: List[JFile]): List[JFile] =
     {
       db.transaction {