src/Pure/Tools/phabricator.scala
changeset 77368 7c57d9586f4c
parent 76540 83de6e9ae983
child 77369 df17355f1e2c
--- a/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -52,7 +52,7 @@
   val default_name = "vcs"
 
   def phabricator_name(name: String = "", ext: String = ""): String =
-    "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
+    "phabricator" + if_proper(name, "-" + name) + if_proper(ext, "." + ext)
 
   def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
     "isabelle-" + phabricator_name(name = name, ext = ext)