# HG changeset patch
# User wenzelm
# Date 1493324503 -7200
# Node ID 7fffa01b2d2b01830b9c0e3cbf50a0087dd999b2
# Parent  ffd8283b7be046c897f3cc28aea30ad4f35c7ec3
proper prefix;

diff -r ffd8283b7be0 -r 7fffa01b2d2b src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Apr 27 16:54:45 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Apr 27 22:21:43 2017 +0200
@@ -17,7 +17,7 @@
   /* log files */
 
   val engine = "build_history"
-  val log_prefix = engine + "-"
+  val log_prefix = engine + "_"
   val META_INFO_MARKER = "\fmeta_info = "