From 8300ef2c07a17451f594bcbd6f0689cafb87c3fb Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 10:40:49 -0500 Subject: Refresh patches --- debian/patches/python-scripts-libraries.patch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian/patches/python-scripts-libraries.patch') 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 -- cgit v1.2.3