equal
deleted
inserted
replaced
147 |
147 |
148 def database_update(options: Options) |
148 def database_update(options: Options) |
149 { |
149 { |
150 val store = Build_Log.store(options) |
150 val store = Build_Log.store(options) |
151 using(store.open_database())(db => |
151 using(store.open_database())(db => |
152 Build_Log.Database.update(store, db, database_dirs, ml_statistics = true, full_view = true)) |
152 Build_Log.Database.update(store, db, database_dirs, ml_statistics = true)) |
153 } |
153 } |
154 |
154 |
155 |
155 |
156 |
156 |
157 /** task logging **/ |
157 /** task logging **/ |