summaryrefslogtreecommitdiff
path: root/debian/libgudhi-dev.install
diff options
context:
space:
mode:
authorGard Spreemann <gspr@nonempty.org>2020-08-11 11:47:59 +0200
committerGard Spreemann <gspr@nonempty.org>2020-08-11 13:36:58 +0200
commitfe7ba81633feafa9232546be4fef18cf37766b1f (patch)
treef1daf94760400d38ba4144b44141e620ca6f1d54 /debian/libgudhi-dev.install
parent4d8c7c21633d6c91f546270887b2c660f7b019d8 (diff)
Build the "user version" of the code.
This is how upstream recommends downstream users build the library.
Diffstat (limited to 'debian/libgudhi-dev.install')
-rw-r--r--debian/libgudhi-dev.install2
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/libgudhi-dev.install b/debian/libgudhi-dev.install
index 47779640..953f5aab 100644
--- a/debian/libgudhi-dev.install
+++ b/debian/libgudhi-dev.install
@@ -1 +1 @@
-build/gudhi/include/gudhi/ usr/include/
+build/userversion/include/gudhi/ usr/include/