# HG changeset patch
# User wenzelm
# Date 1587499455 -7200
# Node ID 5ef7f374e0f8bb0609cd0261edc905da513d0832
# Parent  291c46bf30000daaf511094d31ee13327c6c8933
clarified signature -- avoid warning;

diff -r 291c46bf3000 -r 5ef7f374e0f8 src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Apr 21 19:07:49 2020 +0200
+++ b/src/Pure/General/json.scala	Tue Apr 21 22:04:15 2020 +0200
@@ -29,7 +29,7 @@
 
     def apply(entries: Entry*): Object.T = Map(entries:_*)
 
-    def unapply(obj: T): Option[Object.T] =
+    def unapply(obj: Any): Option[Object.T] =
       obj match {
         case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
           Some(m.asInstanceOf[Object.T])