author | wenzelm |
Tue, 27 Dec 2022 16:36:00 +0100 | |
changeset 76791 | c36d666ee5ee |
parent 76790 | 7a0438979e85 |
child 76792 | 23f433294173 |
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 27 12:15:47 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 27 16:36:00 2022 +0100 @@ -614,7 +614,6 @@ bibtex_entries getOrElse { val text = JEdit_Lib.buffer_text(buffer) val entries = Bibtex.Entries.parse(text, file_pos = node_name.node) - if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors)) bibtex_entries = Some(entries) entries }