diff options
| author | Lucas Nussbaum <lucas@debian.org> | 2017-10-30 13:27:39 +0100 |
|---|---|---|
| committer | Lucas Nussbaum <lucas@debian.org> | 2017-10-30 13:27:39 +0100 |
| commit | e00b39f34c6b2c2444d0c889e15d955d7b62827c (patch) | |
| tree | 02618a0b550659a17e2e495317db96c82079deab | |
| parent | a4c9c6a64ef14e2c3cc3ba7015be9cf3ac2a2f0a (diff) | |
Refresh patch.
| -rw-r--r-- | debian/patches/0004-install-stublibs.patch | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/patches/0004-install-stublibs.patch b/debian/patches/0004-install-stublibs.patch index ee1928f..71167a3 100644 --- a/debian/patches/0004-install-stublibs.patch +++ b/debian/patches/0004-install-stublibs.patch @@ -10,7 +10,7 @@ Subject: Install stublibs +++ b/Makefile @@ -443,10 +443,9 @@ install-libraries: libraries install-lib _build/*.cma _build/*.cmxa _build/*.a _build/*.so \ - `find _build/ -name \*.cmi | grep -v /myocamlbuild` \ + `find _build/ -name \*.cm\[iox\] | grep -v /myocamlbuild` \ `find _build/ -name \*.mli | grep -v /myocamlbuild` \ - $(LIBRARYPREFIX)/$$name/) && \ - if test -d $(LIBRARYPREFIX)/stublibs/; then \ |