summaryrefslogtreecommitdiff
path: root/lib/WriteRepo.hs
diff options
context:
space:
mode:
authorstuebinm2021-11-30 00:19:48 +0100
committerstuebinm2021-11-30 00:19:48 +0100
commitf1c6de8f74c2a410e7ac06df30293060d72fc8a0 (patch)
tree0c399efeea22f6440398522e5712c99d328c733b /lib/WriteRepo.hs
parent72d66169ecef657eae7833c19e80b5e115d4a4b1 (diff)
allow unknown properties
since the scripting API can define new properties and we (for now) do not know what the script may or may not be able to do, the linter would otherwise reject potentially valid maps.
Diffstat (limited to 'lib/WriteRepo.hs')
0 files changed, 0 insertions, 0 deletions