# HG changeset patch
# User wenzelm
# Date 1471206938 -7200
# Node ID 3744d2cf4d2f31c1c6cbcf0f97f996a1ac3591ac
# Parent  2a95d904672ede80896ddd57ad9fd77866181759
proper display of "_";

diff -r 2a95d904672e -r 3744d2cf4d2f src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Sun Aug 14 22:17:32 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Sun Aug 14 22:35:38 2016 +0200
@@ -122,7 +122,7 @@
 set xdata time
 set timefmt "%s"
 set format x "%d-%b"
-set xlabel """ + quote(session) + """
+set xlabel """ + quote(session) + """ noenhanced
 set key left top
 plot [] [0:] """ +
   data_file_name + """ using 1:2 smooth sbezier title "interpolated cpu time",""" +