aboutsummaryrefslogtreecommitdiff
path: root/editors
diff options
context:
space:
mode:
authorFlorian Diebold <[email protected]>2021-05-16 17:27:17 +0100
committerFlorian Diebold <[email protected]>2021-05-21 16:49:09 +0100
commit9716c0b949b1a1a95b3f36928faed3abc21c0bda (patch)
tree3868e00827852afc86162fa82786592378511af5 /editors
parent4bd446f5b3f8035d5db1fde1c6c50073e3f4fb2b (diff)
Deal with goals arising from unification
Diffstat (limited to 'editors')
0 files changed, 0 insertions, 0 deletions