From d11a1268031718a09d7485d3607f10e5e1225d91 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat 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. Gbp-Pq: Name python-scripts-libraries.patch --- tools/CoqMakefile.in | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 403ad617..908929a9 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -90,9 +90,9 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" # 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 ?= -- cgit v1.2.3