diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 10:40:49 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 10:40:49 -0500 |
commit | 8300ef2c07a17451f594bcbd6f0689cafb87c3fb (patch) | |
tree | 91de9118e835c5188b21135dfd9b1cca8c3632a2 /debian/patches/series | |
parent | 6786da162521427921379f05d064c7e47fc2a825 (diff) |
Refresh patches
Diffstat (limited to 'debian/patches/series')
-rw-r--r-- | debian/patches/series | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/patches/series b/debian/patches/series index 2bf642fb..85f4fddd 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -3,7 +3,6 @@ Remove-test-4429.patch Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch 5127-fails-on-mips.patch remove-tests-that-need-coqlib.patch -spelling.patch avoid-usr-bin-env.patch python-scripts-libraries.patch skip-dot-pc.patch |