[make] Escape ORIG_SHELL_PATH to avoid issues due to spaces

Summary:
A space in user's path will lead to a make failure on line 899 of
Makefile. Let's espace the path to avoid that.

Reviewed By: jvillard

Differential Revision: D22044934

fbshipit-source-id: 5a949be1d
master
Artem Pianykh 5 years ago committed by Facebook GitHub Bot
parent fecf954c6e
commit 6ba956d95d

@ -898,7 +898,7 @@ devsetup: Makefile.autoconf
printf "$(TERM_INFO) export BUILD_MODE=dev$(TERM_RESET)\n" >&2; \
printf "$(TERM_INFO) echo 'export BUILD_MODE=dev' >> \"$$shell_config_file\"$(TERM_RESET)\n" >&2; \
fi
$(QUIET)PATH=$(ORIG_SHELL_PATH); if [ "$$(ocamlc -where 2>/dev/null)" != "$$($(OCAMLC) -where)" ]; then \
$(QUIET)PATH='$(ORIG_SHELL_PATH)'; if [ "$$(ocamlc -where 2>/dev/null)" != "$$($(OCAMLC) -where)" ]; then \
echo >&2; \
echo '$(TERM_INFO)*** NOTE: The current shell is not set up for the right opam switch.$(TERM_RESET)' >&2; \
echo '$(TERM_INFO)*** NOTE: Please run:$(TERM_RESET)' >&2; \

Loading…
Cancel
Save