diff options
author | stuebinm | 2021-11-18 21:31:12 +0100 |
---|---|---|
committer | stuebinm | 2021-11-18 21:33:19 +0100 |
commit | d2078f17fe1dad747cc2f14380517bb8402e1347 (patch) | |
tree | cb6a6eab60a50302062fbedb51fe6f9fa310f1d4 /lib/Util.hs | |
parent | e327c7f2ec998a52048136e64ec2c78bc8da75c6 (diff) |
assorted lints for properties found in some maps
(mostly to do with the scripting API, but also some old ones which are
already deprecated / not even mentioned in the documentation anymore)
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions