--- a/src/Pure/Tools/build_log.scala Tue Oct 11 20:31:13 2016 +0200
+++ b/src/Pure/Tools/build_log.scala Tue Oct 11 20:54:42 2016 +0200
@@ -20,6 +20,20 @@
{
/** directory content **/
+ /* file names */
+
+ def log_date(date: Date): String =
+ String.format(Locale.ROOT, "%s.%05d",
+ DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
+ new java.lang.Long((date.time - date.midnight.time).ms / 1000))
+
+ def log_path(engine: String, date: Date, more: String*): Path =
+ Path.explode(date.rep.getYear.toString) +
+ Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+
+
+ /* log file collections */
+
def is_log(file: JFile): Boolean =
List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))