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/python-scripts-libraries.patch | |
| parent | 6786da162521427921379f05d064c7e47fc2a825 (diff) | |
Refresh patches
Diffstat (limited to 'debian/patches/python-scripts-libraries.patch')
| -rw-r--r-- | debian/patches/python-scripts-libraries.patch | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/patches/python-scripts-libraries.patch b/debian/patches/python-scripts-libraries.patch index 66a4a9e9..c4f662a8 100644 --- a/debian/patches/python-scripts-libraries.patch +++ b/debian/patches/python-scripts-libraries.patch @@ -5,7 +5,7 @@ Forwarded: not-needed Eliminate the .py extension from executable Python scripts. --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in -@@ -91,9 +91,9 @@ +@@ -90,9 +90,9 @@ COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts |