diff options
| author | Benjamin Barenblat <bbaren@debian.org> | 2019-08-11 18:33:23 +0200 |
|---|---|---|
| committer | Stéphane Glondu <glondu@debian.org> | 2019-11-08 16:48:46 +0100 |
| commit | d11a1268031718a09d7485d3607f10e5e1225d91 (patch) | |
| tree | 6083f546a35c7a9facb0544c7826a3ed71ccfe6d | |
| parent | ef3448ec0623152c195be10d80ddc91bdf7cfe4e (diff) | |
Differentiate between Python scripts and libraries
Forwarded: not-needed
Eliminate the .py extension from executable Python scripts.
Gbp-Pq: Name python-scripts-libraries.patch
| -rw-r--r-- | tools/CoqMakefile.in | 6 |
1 files 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 ?= |