diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 11:24:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 11:24:23 -0500 |
| commit | 6e23288ca437e8a2761a93da1c09ec52460606aa (patch) | |
| tree | 81d822db80f9724b48f036e725379674412a928f /debian/patches/series | |
| parent | 956960a408a4fe67c7508bf3101d469b6465686d (diff) | |
Disable ssrmatching and ssreflect
The nonfree file in ssrmatching I removed in
cf916fd97fbac51af6fa68ec2704da2a28ef9ede turns out to be important to
the build process, and I can’t figure out how to replicate its effects
without including the file itself. Disable ssrmatching and ssreflect
again until the license situation gets resolved.
Diffstat (limited to 'debian/patches/series')
| -rw-r--r-- | debian/patches/series | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/patches/series b/debian/patches/series index 85f4fddd..3a1b8d0f 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -6,3 +6,4 @@ remove-tests-that-need-coqlib.patch avoid-usr-bin-env.patch python-scripts-libraries.patch skip-dot-pc.patch +remove-ssrmatching.patch |