# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720625477 -7200
# Node ID d507229c5771d2a540d543f3d533e2f571738969
# Parent  17786f08b93e80ea89e9435d8b1026ba1791a03a
proper parse (amending dd86d35375a7);

diff -r 17786f08b93e -r d507229c5771 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Jul 10 17:04:44 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Jul 10 17:31:17 2024 +0200
@@ -17,6 +17,7 @@
   object Component {
     def parse(s: String): Component =
       space_explode('/', s) match {
+        case name :: Nil => Component(name)
         case name :: rev :: Nil => Component(name, rev)
         case _ => error("Malformed component: " + quote(s))
       }