# HG changeset patch
# User wenzelm
# Date 1476561575 -7200
# Node ID 85ad942d1d00451df612af50649cd37dca608d3e
# Parent  ef6f7e8a018c4859cce34a99d29b1c2adaab27d0
more robust quasi-unique name;

diff -r ef6f7e8a018c -r 85ad942d1d00 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Oct 15 21:37:19 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 15 21:59:35 2016 +0200
@@ -194,7 +194,7 @@
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
           Build_Log.log_filename(
-            BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
+            BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads).ext("gz")
 
       val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()