aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
authorErik Martin-Dorel2020-05-28 16:33:33 +0200
committerErik Martin-Dorel2020-05-28 16:37:44 +0200
commit2d16d47667fc9985f315f2dbf62175217f7add1f (patch)
treeaa030babc8a9c78d1b1fac5c7a19eaf27c4969a2 /generic
parent3a5beb79132e23b335f28ab2aef24fa6e587797d (diff)
fix: test files should not provide features
href: https://github.com/ProofGeneral/PG/issues/493#issuecomment-634493988
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions