changeset 65723 | 3ee466e89047 |
parent 65710 | 4326b165b401 |
child 65732 | 7864aea16a87 |
65722:35fcedb6bdc8 | 65723:3ee466e89047 |
---|---|
151 { |
151 { |
152 val store = Build_Log.store(options) |
152 val store = Build_Log.store(options) |
153 using(store.open_database())(db => |
153 using(store.open_database())(db => |
154 { |
154 { |
155 store.update_database(db, database_dirs, ml_statistics = true) |
155 store.update_database(db, database_dirs, ml_statistics = true) |
156 store.snapshot(db, build_log_snapshot) |
156 store.snapshot_database(db, build_log_snapshot) |
157 }) |
157 }) |
158 } |
158 } |
159 |
159 |
160 |
160 |
161 |
161 |