summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-03 17:20:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-05 12:04:05 -0500
commit360aba5ab0b2225dda7d8ab61c62cf7e4baaef53 (patch)
tree4bf246fdb358e6bafacc958714ba3961c7dca497
parent327e96d880445552e44951677b589d8b802b3f06 (diff)
Remove execute bit from Python libraries
-rwxr-xr-xdebian/rules5
1 files changed, 5 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules
index 0aa899e8..1db074b0 100755
--- a/debian/rules
+++ b/debian/rules
@@ -107,6 +107,11 @@ override_dh_install:
chmod +x debian/coq.install
dh_install --fail-missing
+.PHONY: override_dh_fixperms
+override_dh_fixperms:
+ dh_fixperms
+ chmod -x debian/tmp/usr/lib/coq/tools/TimeFileMaker.py
+
.PHONY: override_dh_ocaml
override_dh_ocaml:
dh_ocaml