summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/control1
-rwxr-xr-xdebian/install3
-rwxr-xr-xdebian/rules4
3 files changed, 8 insertions, 0 deletions
diff --git a/debian/control b/debian/control
index 27dd26a..52cd279 100644
--- a/debian/control
+++ b/debian/control
@@ -6,6 +6,7 @@ Build-Depends:
coq (>= 8.4pl1),
coq (<< 8.4pl6),
debhelper (>= 9),
+ dh-exec,
menhir (>= 20140422),
ocaml-nox (>= 4.00.0)
Standards-Version: 3.9.6
diff --git a/debian/install b/debian/install
new file mode 100755
index 0000000..500b0dd
--- /dev/null
+++ b/debian/install
@@ -0,0 +1,3 @@
+#!/usr/bin/dh-exec
+_build/driver/Driver.native => usr/bin/ccomp
+runtime/libcompcert.a usr/lib/${DEB_HOST_MULTIARCH}
diff --git a/debian/rules b/debian/rules
index fd43eb3..e49cab6 100755
--- a/debian/rules
+++ b/debian/rules
@@ -22,6 +22,10 @@ override_dh_auto_build:
-prefix /usr -libdir /usr/lib/$(DEB_HOST_MULTIARCH) ia32-linux
dh_auto_build
+.PHONY: override_dh_auto_install
+override_dh_auto_install:
+ /bin/true
+
.PHONY: override_dh_builddeb
override_dh_builddeb:
dh_builddeb -- -Zxz -z9