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
@@ -90,9 +90,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 ?=