blob: 66a4a9e9acd357b1ea4e32f60ad4e4569949ff8f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
From: Benjamin Barenblat <bbaren@debian.org>
Subject: Differentiate between Python scripts and libraries
Forwarded: not-needed
Eliminate the .py extension from executable Python scripts.
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -91,9 +91,9 @@
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 ?=
|
