# HG changeset patch
# User wenzelm
# Date 1631715113 -7200
# Node ID 7b860fa1140f7ae83249b548a6c3fb9b6dcc11c0
# Parent  19022ea3f8cc587c138ebbbd0a63f7eba08e40a8
tuned;

diff -r 19022ea3f8cc -r 7b860fa1140f src/Pure/Admin/build_vampire.scala
--- 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 */