--- a/src/Pure/Admin/build_stats.scala Sat May 06 12:52:29 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala Sat May 06 12:59:16 2017 +0200
@@ -63,7 +63,7 @@
using(store.open_database())(db =>
{
for (profile <- profiles) {
- progress.echo("database query " + quote(profile.name))
+ progress.echo("input " + quote(profile.name))
val columns =
List(
Build_Log.Data.pull_date,
@@ -145,7 +145,7 @@
val data_entries = data.toList.sortBy(_._1)
for ((name, session_entries) <- data_entries) {
val dir = target_dir + Path.explode(name)
- progress.echo("directory " + dir)
+ progress.echo("output " + dir)
Isabelle_System.mkdirs(dir)
for ((session, entries) <- session_entries) {
@@ -196,7 +196,7 @@
val result =
Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
if (result.rc != 0)
- result.error("Gnuplot error in " + name + "/" + session).check
+ result.error("Gnuplot failed for " + name + "/" + session).check
}
}
}