src/Pure/Tools/phabricator.scala
changeset 71601 97ccf48c2f0c
parent 71550 f2b944898636
child 71726 a5fda30edae2
equal deleted inserted replaced
71600:64aad1e46f98 71601:97ccf48c2f0c
    37 
    37 
    38   val www_user = "www-data"
    38   val www_user = "www-data"
    39 
    39 
    40   val daemon_user = "phabricator"
    40   val daemon_user = "phabricator"
    41 
    41 
    42   val sshd_config = Path.explode("/etc/ssh/sshd_config")
    42   val sshd_config: Path = Path.explode("/etc/ssh/sshd_config")
    43 
    43 
    44 
    44 
    45   /* installation parameters */
    45   /* installation parameters */
    46 
    46 
    47   val default_name = "vcs"
    47   val default_name = "vcs"
    57 
    57 
    58   def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
    58   def default_repo(name: String): Path = default_root(name) + Path.basic("repo")
    59 
    59 
    60   val default_mailers: Path = Path.explode("mailers.json")
    60   val default_mailers: Path = Path.explode("mailers.json")
    61 
    61 
    62   val default_system_port = SSH.default_port
    62   val default_system_port: Int = SSH.default_port
    63   val alternative_system_port = 222
    63   val alternative_system_port = 222
    64   val default_server_port = 2222
    64   val default_server_port = 2222
    65 
    65 
    66   val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
    66   val standard_mercurial_source = "https://www.mercurial-scm.org/release/mercurial-3.9.2.tar.gz"
    67 
    67 
    68 
    68 
    69 
    69 
    70   /** global configuration **/
    70   /** global configuration **/
    71 
    71 
    72   val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
    72   val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
    73 
    73 
    74   def global_config_script(
    74   def global_config_script(
    75     init: String = "",
    75     init: String = "",
    76     body: String = "",
    76     body: String = "",
    77     exit: String = ""): String =
    77     exit: String = ""): String =