clarified default, following 8b695e59db3f;
authorwenzelm
Fri, 16 Sep 2022 15:07:33 +0200
changeset 76173 5298a498738c
parent 76172 81241a1d3d99
child 76174 c8ab2316e3cb
clarified default, following 8b695e59db3f;
src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Sep 16 15:05:50 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala	Fri Sep 16 15:07:33 2022 +0200
@@ -889,8 +889,7 @@
 
     /* context for operations */
 
-    def apply(server: String, port: Int = default_system_port): API =
-      new API(server, port)
+    def apply(server: String, port: Int = 0): API = new API(server, port)
   }
 
   final class API private(server: String, port: Int) {