--- a/src/Pure/Tools/build.scala Mon Mar 06 16:06:24 2023 +0100
+++ b/src/Pure/Tools/build.scala Mon Mar 06 16:20:12 2023 +0100
@@ -323,10 +323,10 @@
soft_build = soft_build,
export_files = export_files)
}
- val end_date = Date.now()
- val elapsed_time = end_date.time - start_date.time
+ val stop_date = Date.now()
+ val elapsed_time = stop_date.time - start_date.time
- progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
+ progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true)
val total_timing =
results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
--- a/src/Pure/Tools/build_process.scala Mon Mar 06 16:06:24 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Mar 06 16:20:12 2023 +0100
@@ -276,9 +276,9 @@
val ml_platform = SQL.Column.string("ml_platform")
val options = SQL.Column.string("options")
val start = SQL.Column.date("start")
- val end = SQL.Column.date("end")
+ val stop = SQL.Column.date("stop")
- val table = make_table("", List(build_uuid, ml_platform, options, start, end))
+ val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
}
def start_build(
@@ -297,15 +297,15 @@
})
}
- def end_build(db: SQL.Database, build_uuid: String): Unit =
+ def stop_build(db: SQL.Database, build_uuid: String): Unit =
db.execute_statement(
- Base.table.update(List(Base.end), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+ Base.table.update(List(Base.stop), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
body = { stmt => stmt.date(1) = db.now() })
def clean_build(db: SQL.Database): Unit = {
val old =
db.using_statement(
- Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.end.defined))
+ Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined))
)(stmt => stmt.execute_query().iterator(_.string(Base.build_uuid)).toList)
if (old.nonEmpty) {
@@ -827,7 +827,7 @@
def exit(): Unit = synchronized_database {
for (db <- _database) {
- Build_Process.Data.end_build(db, build_uuid)
+ Build_Process.Data.stop_build(db, build_uuid)
}
}