# HG changeset patch
# User wenzelm
# Date 1573120205 -3600
# Node ID 9ce299019d21a268516f85e4254be23421e37d7d
# Parent  79b89278b8252b84e4b6e88f834bfb4788a693a5
tuned message;

diff -r 79b89278b825 -r 9ce299019d21 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Thu Nov 07 10:47:33 2019 +0100
+++ b/src/Pure/Tools/phabricator.scala	Thu Nov 07 10:50:05 2019 +0100
@@ -419,7 +419,8 @@
       }
       if (File.read(default_config_file) == mailers_template) {
         progress.echo(
-          "Please invoke the tool again, after providing details in\n  " + default_config_file)
+          "Please invoke the tool again, after providing details in:\n  " +
+          default_config_file.implode)
       }
       else setup_mail
     }