src/Tools/jEdit/src/jedit_bibtex.scala
changeset 67290 98b6cd12f963
parent 66152 18e1aba549f6
child 73617 20d0abffee99
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -35,7 +35,7 @@
       case text_area: TextArea =>
         text_area.getBuffer match {
           case buffer: Buffer
-          if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
+          if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
             for (entry <- Bibtex.known_entries) {
               val item = new JMenuItem(entry.kind)