diff options
Diffstat (limited to 'debian')
| -rwxr-xr-x | debian/rules | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index e49cab6..dd00125 100755 --- a/debian/rules +++ b/debian/rules @@ -7,21 +7,26 @@ export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed %: dh $@ --parallel +# make clean won't work unless there's already a Makefile.config. Create one +# before trying to clean. .PHONY: override_dh_auto_clean override_dh_auto_clean: touch Makefile.config dh_auto_clean +# The configure script distributed with CompCert is totally nonstandard. We'll +# run it manually. .PHONY: override_dh_auto_configure override_dh_auto_configure: /bin/true - .PHONY: override_dh_auto_build override_dh_auto_build: ./configure \ -prefix /usr -libdir /usr/lib/$(DEB_HOST_MULTIARCH) ia32-linux dh_auto_build +# The default installation procedure is fairly inflexible. We'll just install +# everything manually. .PHONY: override_dh_auto_install override_dh_auto_install: /bin/true |