diff options
Diffstat (limited to 'debian/install')
-rwxr-xr-x | debian/install | 3 |
1 files changed, 3 insertions, 0 deletions
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} |