# HG changeset patch
# User wenzelm
# Date 1525640505 -7200
# Node ID 0c7820590236240f24aa6bf9c0e9d15ed9ca0594
# Parent  7c8ed28dd40a207e368b9956ca427d02bb7954c3
tuned signature;

diff -r 7c8ed28dd40a -r 0c7820590236 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun May 06 22:15:52 2018 +0200
+++ b/src/Pure/General/sql.scala	Sun May 06 23:01:45 2018 +0200
@@ -120,7 +120,8 @@
     def defined: String = ident + " IS NOT NULL"
     def undefined: String = ident + " IS NULL"
 
-    def where_equal(s: String): Source = "WHERE " + ident + " = " + string(s)
+    def equal(s: String): Source = ident + " = " + string(s)
+    def where_equal(s: String): Source = "WHERE " + equal(s)
 
     override def toString: Source = ident
   }
diff -r 7c8ed28dd40a -r 0c7820590236 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Sun May 06 22:15:52 2018 +0200
+++ b/src/Pure/System/process_result.scala	Sun May 06 23:01:45 2018 +0200
@@ -15,7 +15,8 @@
 {
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
-  def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
+  def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs)
+  def error(err: String): Process_Result = errors(List(err))
 
   def was_timeout: Process_Result = copy(rc = 1, timeout = true)