# HG changeset patch
# User wenzelm
# Date 1730660454 -3600
# Node ID 0ec5131899b679a8aa721e399dc76bda91a406f4
# Parent  33fbf90fbc1df258f450411bff73baf8540e72cd
unused;

diff -r 33fbf90fbc1d -r 0ec5131899b6 src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Sun Nov 03 19:38:30 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Sun Nov 03 20:00:54 2024 +0100
@@ -15,7 +15,6 @@
 import java.awt.event.{ActionListener, ActionEvent}
 
 import javax.swing.text.Segment
-import javax.swing.tree.DefaultMutableTreeNode
 import javax.swing.{JMenu, JMenuItem}
 
 import org.gjt.sp.jedit.Buffer