diff options
Diffstat (limited to 'debian/gbp.conf')
| -rw-r--r-- | debian/gbp.conf | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debian/gbp.conf b/debian/gbp.conf index f9ed7826..a4ee2a5f 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -55,4 +55,7 @@ filter = [ # 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/ssrmatching.v", + + # This tries to build upstream's CI on Salsa, which doesn't work. + ".travis.yml" ] |