# HG changeset patch
# User wenzelm
# Date 1493384806 -7200
# Node ID e6e3fed86519ea1efd13fb4505ef1e3131ebb751
# Parent  9917b8e3b5c12d517bf9caca32ee6f0fddebc3f2
allow null;

diff -r 9917b8e3b5c1 -r e6e3fed86519 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Apr 28 14:50:18 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri Apr 28 15:06:46 2017 +0200
@@ -216,7 +216,10 @@
     def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
     def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
     def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
-    { stmt.setBinaryStream(i, bytes.stream(), bytes.length) }
+    {
+      if (bytes == null) stmt.setBytes(i, null)
+      else stmt.setBinaryStream(i, bytes.stream(), bytes.length)
+    }
     def set_date(stmt: PreparedStatement, i: Int, date: Date)