--- a/src/Tools/jEdit/src/jedit_bibtex.scala Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Fri Aug 19 16:46:00 2022 +0200
@@ -29,7 +29,7 @@
def context_menu(text_area: JEditTextArea): List[JMenuItem] = {
text_area.getBuffer match {
case buffer: Buffer
- if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
+ if File.is_bib(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
val menu = new JMenu("BibTeX entries")
for (entry <- Bibtex.known_entries) {
val item = new JMenuItem(entry.kind)