diff options
Diffstat (limited to 'debian/patches/series')
| -rw-r--r-- | debian/patches/series | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/patches/series b/debian/patches/series index 393f2c14..16c98dbc 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -4,8 +4,8 @@ remove-tests-that-need-coqlib.patch avoid-usr-bin-env.patch python-scripts-libraries.patch skip-dot-pc.patch -remove-ssrmatching.patch spelling.patch verbose-build.patch fix-bytecode-build.patch remove-bytecode-failing-tests.patch +ssrmatching-license.patch |