summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2020-06-23 14:39:39 +0100
committerGitHub <noreply@github.com>2020-06-23 14:39:39 +0100
commit6fc8e07d62881d4c07f89b77a7f9b91e38e4c2d6 (patch)
tree94dda1598001606863c5e7637724931b05ff0907 /tools
parentf0fae6692f7945ddcc8ab1267fdcb22b9e2fe40e (diff)
parentafcac60650ed08d25283107f13d28ce87de41b5c (diff)
downloadocaml-6fc8e07d62881d4c07f89b77a7f9b91e38e4c2d6.tar.gz
Merge pull request #9692 from nojb/shellquote
Simplify Makefile
Diffstat (limited to 'tools')
-rw-r--r--tools/Makefile7
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