diff options
Diffstat (limited to 'debian/rules')
| -rwxr-xr-x | debian/rules | 5 |
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 |