From bac5683a8429042f04a0f60643f6f0d1983b7842 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Thu, 17 Jan 2019 16:33:19 -0500 Subject: Don’t build upstream’s CI on Salsa MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- debian/gbp.conf | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'debian') 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" ] -- cgit v1.2.3