diff options
author | Gard Spreemann <gspr@nonempty.org> | 2020-08-11 11:47:59 +0200 |
---|---|---|
committer | Gard Spreemann <gspr@nonempty.org> | 2020-08-11 13:36:58 +0200 |
commit | fe7ba81633feafa9232546be4fef18cf37766b1f (patch) | |
tree | f1daf94760400d38ba4144b44141e620ca6f1d54 /debian/libgudhi-dev.install | |
parent | 4d8c7c21633d6c91f546270887b2c660f7b019d8 (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.install | 2 |
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/ |