changeset 77368 | 7c57d9586f4c |
parent 77028 | f5896dea6fce |
--- a/src/Pure/PIDE/resources.scala Fri Feb 24 20:23:48 2023 +0100 +++ b/src/Pure/PIDE/resources.scala Fri Feb 24 20:40:50 2023 +0100 @@ -308,8 +308,7 @@ "Cyclic dependency of " + show_path(names) private def required_by(initiators: List[Document.Node.Name]): String = - if (initiators.isEmpty) "" - else "\n(required by " + show_path(initiators.reverse) + ")" + if_proper(initiators, "\n(required by " + show_path(initiators.reverse) + ")") } final class Dependencies[A] private(