author | wenzelm |
Wed, 15 Sep 2021 16:11:53 +0200 | |
changeset 74312 | 7b860fa1140f |
parent 74311 | 19022ea3f8cc |
child 74313 | 6b998ce1b8cb |
--- a/src/Pure/Admin/build_vampire.scala Wed Sep 15 16:02:04 2021 +0200 +++ b/src/Pure/Admin/build_vampire.scala Wed Sep 15 16:11:53 2021 +0200 @@ -14,7 +14,7 @@ val default_version2 = "df87588848db" val default_jobs = 1 - def make_component_name(version: String) = "vampire-" + version + def make_component_name(version: String): String = "vampire-" + version /* build Vampire */