--- a/src/Pure/Thy/sessions.scala Thu Aug 25 23:09:00 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Aug 26 11:41:59 2022 +0200
@@ -167,7 +167,7 @@
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
- progress.echo("Session " + info.chapter_session + groups)
+ progress.echo("Session " + info.chapter + "/" + session_name + groups)
}
val dependencies = resources.session_dependencies(info)
@@ -477,8 +477,6 @@
export_classpath: List[String],
meta_digest: SHA1.Digest
) {
- def chapter_session: String = chapter + "/" + name
-
def deps: List[String] = parent.toList ::: imports
def deps_base(session_bases: String => Base): Base = {