diff options
Diffstat (limited to 'debian/gbp.conf')
| -rw-r--r-- | debian/gbp.conf | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/debian/gbp.conf b/debian/gbp.conf index a4ee2a5f..92f87323 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -51,11 +51,7 @@ filter = [ # Code with CeCILL-B license headers. bbaren believes CeCILL-B to be # nonfree; see # https://lists.debian.org/msgid-search/875zvih02a.jfx@benwick.benjamin.barenblat.name. - # - # These files will be patched in with properly licensed replacements once - # https://github.com/coq/coq/pull/9282 is merged. - "plugins/ssrmatching/ssrmatching.mli", - "plugins/ssrmatching/ssrmatching.v", + "plugins/ssrmatching/g_ssrmatching.mli", # This tries to build upstream's CI on Salsa, which doesn't work. ".travis.yml" ] |