diff options
author | David Allsopp <david.allsopp@metastack.com> | 2020-06-23 14:39:39 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-23 14:39:39 +0100 |
commit | 6fc8e07d62881d4c07f89b77a7f9b91e38e4c2d6 (patch) | |
tree | 94dda1598001606863c5e7637724931b05ff0907 /tools | |
parent | f0fae6692f7945ddcc8ab1267fdcb22b9e2fe40e (diff) | |
parent | afcac60650ed08d25283107f13d28ce87de41b5c (diff) | |
download | ocaml-6fc8e07d62881d4c07f89b77a7f9b91e38e4c2d6.tar.gz |
Merge pull request #9692 from nojb/shellquote
Simplify Makefile
Diffstat (limited to 'tools')
-rw-r--r-- | tools/Makefile | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tools/Makefile b/tools/Makefile index 69b67c586e..931ec3eeeb 100644 --- a/tools/Makefile +++ b/tools/Makefile @@ -18,13 +18,6 @@ ROOTDIR = .. include $(ROOTDIR)/Makefile.common -ifeq ($(SYSTEM),unix) -override define shellquote -$i := $$(subst ",\",$$(subst $$$$,\$$$$,$$(subst `,\`,$i)))#")# -endef -$(foreach i,BINDIR LIBDIR STUBLIBDIR MANDIR,$(eval $(shellquote))) -endif - DESTDIR ?= # Setup GNU make variables storing per-target source and target, # a list of installed tools, and a function to quote a filename for |