author | wenzelm |
Tue, 23 Jan 2024 20:10:40 +0100 | |
changeset 79522 | 08ef19aacced |
parent 79521 | db2b5c04075d |
child 79523 | f1287f1894a0 |
--- 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]