diff -r 6cc3b131f761 -r ee7dc5151db5 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Mon Feb 06 16:11:05 2023 +0100 +++ b/src/Pure/Thy/document_build.scala Mon Feb 06 16:21:25 2023 +0100 @@ -228,7 +228,7 @@ lazy val session_tex: File.Content = { val path = Path.basic("session.tex") val content = - Library.terminate_lines( + terminate_lines( session_document_theories.map(name => "\\input{" + tex_name(name) + "}")) File.content(path, content) }