Merge branch 'master' into develop

This commit is contained in:
Pieter Vander Vennet 2022-08-18 19:18:45 +02:00
commit 2cdb7f332e
8 changed files with 176 additions and 23 deletions

View file

@ -14,8 +14,6 @@ import List from "../../UI/Base/List";
import {MappingConfigJson, QuestionableTagRenderingConfigJson} from "./Json/QuestionableTagRenderingConfigJson";
import {FixedUiElement} from "../../UI/Base/FixedUiElement";
import {Paragraph} from "../../UI/Base/Paragraph";
import spec = Mocha.reporters.spec;
import SpecialVisualizations from "../../UI/SpecialVisualizations";
export interface Mapping {
readonly if: TagsFilter,