# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700144621 -3600
# Node ID d5ce982ae60f4782d94dd5b0373b4cd2d672acf3
# Parent  80fda74a045d500b03dc8f501bef5742920c3df3
allow re-defining keys in toml object (already checked during parse time);

diff -r 80fda74a045d -r d5ce982ae60f src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Thu Nov 16 15:19:24 2023 +0100
+++ b/src/Pure/General/toml.scala	Thu Nov 16 15:23:41 2023 +0100
@@ -137,7 +137,7 @@
           (v0, v) match {
             case (t0: Table, t: Table) => t0 ++ t
             case (a0: Array, a: Array) => a0 ++ a
-            case _ => error("Key already present: " + Format.key(k))
+            case _ => v
           }
       }
       new Table(rep + (k -> v1))