changeset 78894 | 1fbfe0bca5e1 |
parent 78880 | 9ce8bf038444 |
child 78900 | 9f7a94117666 |
--- 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) } }