diff options
| author | stuebinm | 2021-11-30 00:19:48 +0100 |
|---|---|---|
| committer | stuebinm | 2021-11-30 00:19:48 +0100 |
| commit | f1c6de8f74c2a410e7ac06df30293060d72fc8a0 (patch) | |
| tree | 0c399efeea22f6440398522e5712c99d328c733b /lib/WriteRepo.hs | |
| parent | 72d66169ecef657eae7833c19e80b5e115d4a4b1 (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