diff options
Diffstat (limited to 'debian/rules')
-rwxr-xr-x | debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index 379cb28f..4ed4e3a3 100755 --- a/debian/rules +++ b/debian/rules @@ -83,7 +83,7 @@ override_dh_auto_install: .PHONY: override_dh_install override_dh_install: - dh_install --list-missing + dh_install --fail-missing cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm .PHONY: override_dh_gencontrol |