# HG changeset patch
# User wenzelm
# Date 1710107718 -3600
# Node ID ea5b1f0cb448178b7d3069d0ed11bc94cc51cfce
# Parent  9cb5e20df9a4a2e48393c4c3f0a986ced7edd525
unused (see 123f2c0995b8);

diff -r 9cb5e20df9a4 -r ea5b1f0cb448 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Mar 10 22:42:27 2024 +0100
+++ b/src/Pure/General/sql.scala	Sun Mar 10 22:55:18 2024 +0100
@@ -57,7 +57,6 @@
 
   val join_outer: Source = " LEFT OUTER JOIN "
   val join_inner: Source = " INNER JOIN "
-  def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
   def MULTI(args: Iterable[Source]): Source =
     args.iterator.filter(_.nonEmpty).mkString(";\n")