tuned whitespace;
authorwenzelm
Wed, 15 Dec 2021 19:39:02 +0100
changeset 74944 9b14491ca5c6
parent 74943 afd8cb7b2be1
child 74945 4dc90b43ba94
tuned whitespace;
src/Pure/Tools/phabricator.scala
--- 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] =