# HG changeset patch
# User wenzelm
# Date 1705839485 -3600
# Node ID e82448aacf48cef7cf459e8fe894e87be2f64e78
# Parent  b2861a2c2aa26b1b8282971bd7454edb77879c3d
unused;

diff -r b2861a2c2aa2 -r e82448aacf48 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jan 20 22:27:30 2024 +0100
+++ b/src/Pure/General/bytes.scala	Sun Jan 21 13:18:05 2024 +0100
@@ -9,7 +9,6 @@
 
 import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream,
   InputStream, OutputStream, File => JFile}
-import java.net.URL
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption