diff options
author | 2019-02-02 18:59:45 -0500 | |
---|---|---|
committer | 2019-02-02 19:12:56 -0500 | |
commit | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (patch) | |
tree | bab0e7c4c39ed4180c086964ba0593f995fe3d42 /tactics/btermdn.ml | |
parent | cf916fd97fbac51af6fa68ec2704da2a28ef9ede (diff) |
Prepare gbp to import 8.9.0
8.9.0 deleted some files under non-DFSG-free licenses, so we no longer
need to filter out those files when importing.
Diffstat (limited to 'tactics/btermdn.ml')
0 files changed, 0 insertions, 0 deletions