From 19ca9065d62878287a4f9715a711aa8487276e56 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 29 Nov 2023 11:15:24 +0100 Subject: [PATCH] Set default union domain to map. --- src/common/util/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 95668758a5..7298e6dd88 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -757,7 +757,7 @@ "The domain that should be used for unions. Options: simple/map", "type": "string", "enum": ["simple", "map"], - "default": "simple" + "default": "map" } }, "additionalProperties": false