# HG changeset patch
# User wenzelm
# Date 1698316030 -7200
# Node ID 3958180eaa7253536802ccfdb585d95fff3c5a77
# Parent  966aa081929fdc892de8b042352ee5bc7a5b6f3a
tuned signature;

diff -r 966aa081929f -r 3958180eaa72 src/Pure/System/host.scala
--- a/src/Pure/System/host.scala	Thu Oct 26 11:50:50 2023 +0200
+++ b/src/Pure/System/host.scala	Thu Oct 26 12:27:10 2023 +0200
@@ -40,7 +40,7 @@
         case _ => None
       }
 
-    def from(s: String) =
+    def from(s: String): List[Int] =
       s match {
         case Range(r) => r
         case _ => Nil