src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Wed Nov 14 11:51:03 2018 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 14 16:26:58 2018 +0100
@@ -141,7 +141,7 @@
 
   def read_dir(dir: Path): List[String] =
   {
-    if (!dir.is_dir) error("Bad directory: " + dir.toString)
+    if (!dir.is_dir) error("No such directory: " + dir.toString)
     val files = dir.file.listFiles
     if (files == null) Nil
     else files.toList.map(_.getName)