diff options
| author | Stefano Zacchiroli <zack@debian.org> | 2017-08-08 17:40:35 +0200 |
|---|---|---|
| committer | Stéphane Glondu <glondu@debian.org> | 2023-09-02 09:51:27 +0200 |
| commit | 7a891059413194a22cd3dfa707ef3a7444cffc33 (patch) | |
| tree | c6670518ceb7a7b0ca9442d12e3c69dfa237f4bf | |
| parent | 9b972b0f8a33f00c09639832736d5c3d4fb99336 (diff) | |
Enable installing to a target directory passed from debian/rules
Gbp-Pq: Name 0001-Enable-installing-to-a-target-directory-passed-from-.patch
| -rw-r--r-- | Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -17,6 +17,7 @@ XARCHIVE = xstr.cmxa NAME = xstr #REQUIRES = UNSAFE = +DESTDIR = # you may try this: (0% to 10% faster) #UNSAFE = -unsafe @@ -48,8 +49,9 @@ depend: *.ml *.mli .PHONY: install install: all + if [ ! -d $(DESTDIR) ] ; then mkdir -p $(DESTDIR) ; fi { test ! -f $(XARCHIVE) || extra="*.cmxa *.a"; }; \ - $(OCAMLFIND) install $(NAME) *.mli *.cmi *.cma META $$extra + $(OCAMLFIND) install -destdir $(DESTDIR) $(NAME) *.mli *.cmi *.cma META $$extra .PHONY: uninstall uninstall: |