clarified check: this could be \nocite;
authorwenzelm
Fri, 13 Jan 2023 12:16:04 +0100
changeset 76958 d9727629cb67
parent 76957 deb7dffb3340
child 76959 3d491a0af6ef
clarified check: this could be \nocite;
src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Thu Jan 12 20:09:08 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 13 12:16:04 2023 +0100
@@ -57,7 +57,7 @@
             if null bibtex_entries andalso thy_name <> Context.PureN then ()
             else
               citations |> List.app (fn (name, pos) =>
-                if member (op =) bibtex_entries name then ()
+                if member (op =) bibtex_entries name orelse name = "*" then ()
                 else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
           val kind = Config.get ctxt cite_macro;