src/Pure/Thy/sessions.scala
changeset 77035 28ac56e59d23
parent 77030 d7dc5b1e4381
child 77038 7b5b1789a34c
--- 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)