diff options
| author | Gard Spreemann <gspreemann@gmail.com> | 2018-06-12 10:51:06 +0200 |
|---|---|---|
| committer | Gard Spreemann <gspreemann@gmail.com> | 2018-06-12 11:32:00 +0200 |
| commit | b6d352a83740be5ce12e33b0b89980538246a504 (patch) | |
| tree | 8f7b9a41ec89242bf5112ad1db82c331785138ce /debian/gudhi-utils.install | |
| parent | 9f3023fc3e5cb3fa7073d5b3fa2c7011002af1d1 (diff) | |
Install utilities (binary gudhi-utils).
Diffstat (limited to 'debian/gudhi-utils.install')
| -rw-r--r-- | debian/gudhi-utils.install | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/gudhi-utils.install b/debian/gudhi-utils.install new file mode 100644 index 00000000..71e8eb9f --- /dev/null +++ b/debian/gudhi-utils.install @@ -0,0 +1 @@ +debian/tmp/usr/bin/gudhi-* usr/bin/ |