# HG changeset patch
# User wenzelm
# Date 1494063815 -7200
# Node ID 6bfe25513851835cb3e67a64db5c60814a83fccf
# Parent  0729c09be90cbbb58f243fa321e00ec15eb1530a
tuned;

diff -r 0729c09be90c -r 6bfe25513851 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat May 06 00:23:04 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat May 06 11:43:35 2017 +0200
@@ -977,9 +977,9 @@
         if (ml_statistics) {
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
-            SQL.join_outer(table1, table2,
-              Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
-              Data.session_name(table1) + " = " + Data.session_name(table2))
+            table1 + " LEFT OUTER JOIN " + table2 + " ON " +
+            Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
+            Data.session_name(table1) + " = " + Data.session_name(table2)
           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)