Package: coq / 8.12.0-3

python-scripts-libraries.patch Patch series | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sun, 11 Aug 2019 18:33:23 +0200
Subject: Differentiate between Python scripts and libraries

Forwarded: not-needed

Eliminate the .py extension from executable Python scripts.
---
 tools/CoqMakefile.in | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

Index: coq/tools/CoqMakefile.in
===================================================================
--- coq.orig/tools/CoqMakefile.in	2020-08-21 13:11:23.171956803 +0200
+++ coq/tools/CoqMakefile.in	2020-08-21 13:11:23.167956803 +0200
@@ -97,9 +97,9 @@
 OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
 
 # Timing scripts
-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files"
 BEFORE ?=
 AFTER ?=