diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-01-17 16:33:19 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-01-17 16:33:19 -0500 |
| commit | bac5683a8429042f04a0f60643f6f0d1983b7842 (patch) | |
| tree | 5eddfa9730d3b7b185837bf6ced8ce430ff6daea /debian | |
| parent | 11d2b496980a65ac1059b72275480d572634d13f (diff) | |
Don’t build upstream’s CI on Salsa
Diffstat (limited to 'debian')
| -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" ] |