# HG changeset patch
# User wenzelm
# Date 1605968412 -3600
# Node ID 573ccec4dbac3194baff1e32e89985fde8535fae
# Parent  588c751a5eef448e1b318624bd9077e4f221ff40
tuned signature;

diff -r 588c751a5eef -r 573ccec4dbac src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Nov 21 00:29:41 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Nov 21 15:20:12 2020 +0100
@@ -497,7 +497,7 @@
         case doc => error("Bad document specification " + quote(doc))
       }
 
-    def documents_variants: List[Presentation.Document_Variant] =
+    def document_variants: List[Presentation.Document_Variant] =
     {
       val variants =
         Library.space_explode(':', options.string("document_variants")).
@@ -511,7 +511,7 @@
 
     def documents: List[Presentation.Document_Variant] =
     {
-      val variants = documents_variants
+      val variants = document_variants
       if (!document_enabled || document_files.isEmpty) Nil else variants
     }