author | wenzelm |
Wed, 15 Dec 2021 19:39:02 +0100 | |
changeset 74944 | 9b14491ca5c6 |
parent 74943 | afd8cb7b2be1 |
child 74945 | 4dc90b43ba94 |
--- a/src/Pure/Tools/phabricator.scala Wed Dec 15 19:30:57 2021 +0100 +++ b/src/Pure/Tools/phabricator.scala Wed Dec 15 19:39:02 2021 +0100 @@ -876,7 +876,7 @@ val hg, git, svn = Value def read(s: String): Value = try { withName(s) } - catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } + catch { case _: java.util.NoSuchElementException => error("Unknown vcs type " + quote(s)) } } def edits(typ: String, value: JSON.T): List[JSON.Object.T] =