# HG changeset patch
# User wenzelm
# Date 1595596835 -7200
# Node ID ebf3ba74bc4c0d1bf7fd0ba1e438be4c7a5eff09
# Parent  4768b1facec2367417ff61d26011f37979b67505
unused;

diff -r 4768b1facec2 -r ebf3ba74bc4c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Jul 24 15:02:16 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Jul 24 15:20:35 2020 +0200
@@ -7,7 +7,6 @@
 package isabelle
 
 
-import scala.annotation.tailrec
 import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}