proper Apache.php_name;
authorwenzelm
Tue, 23 Jan 2024 20:10:40 +0100
changeset 79522 08ef19aacced
parent 79521 db2b5c04075d
child 79523 f1287f1894a0
proper Apache.php_name;
src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Jan 23 19:56:52 2024 +0100
+++ b/src/Pure/Tools/phabricator.scala	Tue Jan 23 20:10:40 2024 +0100
@@ -59,7 +59,7 @@
     def title: String
     def short_name: String
     def system_name: String = short_name
-    def php_name: String = short_name
+    def php_name: String = system_name
 
     def packages(): List[String]