author | wenzelm |
Sat, 04 Nov 2023 16:07:22 +0100 | |
changeset 78894 | 1fbfe0bca5e1 |
parent 78893 | 3645442be6d5 |
child 78895 | 801f8237cc5e |
--- a/src/Pure/Admin/build_log.scala Fri Nov 03 19:10:21 2023 +0100 +++ b/src/Pure/Admin/build_log.scala Sat Nov 04 16:07:22 2023 +0100 @@ -1211,7 +1211,7 @@ if (errors.isEmpty) { for (path <- snapshot) { - progress.echo("Writing database snapshot " + path) + progress.echo("Writing database snapshot " + path.expand) store.snapshot_database(db, path) } }