--- a/src/Pure/Thy/sessions.scala Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jan 20 21:56:34 2023 +0100
@@ -1386,9 +1386,9 @@
/* file names */
def heap(name: String): Path = Path.basic(name)
- def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
+ def database(name: String): Path = Path.basic("log") + Path.basic(name).db
def log(name: String): Path = Path.basic("log") + Path.basic(name)
- def log_gz(name: String): Path = log(name).ext("gz")
+ def log_gz(name: String): Path = log(name).gz
def output_heap(name: String): Path = output_dir + heap(name)
def output_database(name: String): Path = output_dir + database(name)