src/Pure/Admin/build_log.scala
changeset 65632 218dbe4fb484
parent 65631 ee917f172912
child 65633 826311fca263
--- 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 {