# HG changeset patch
# User wenzelm
# Date 1605177787 -3600
# Node ID e00089ddf462a4e296b877b86a95413eba3c86b2
# Parent  18eb7ec2720f9beb12623456d606c932364c96d4
tuned imports;

diff -r 18eb7ec2720f -r e00089ddf462 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Thu Nov 12 11:00:34 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala	Thu Nov 12 11:43:07 2020 +0100
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import java.io.{File => JFile}
-
-
 object Build_Doc
 {
   /* build_doc */