aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2020-02-25 13:53:03 +0100
committerHugo Herbelin2020-02-28 05:35:56 +0100
commita4d8c9414e65271fc97347ae04b0b431206d33f8 (patch)
treef9510503c5d2bdde643a4e4121fa793f9a9e6651
parent02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 (diff)
Makefile in test-suite: More separation of concerns as suggested by Enrico.
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
-rw-r--r--test-suite/Makefile10
1 files changed, 7 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6a6b729578..1681150f7b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -32,11 +32,15 @@ include ../Makefile.common
# Variables
#######################################################################
+# Using quotes to anticipate the possibility of spaces in the directory name
+# Note that this will later need an eval in shell to interpret the quotes
+ROOT='$(shell cd ..; pwd)'
+
ifneq ($(wildcard ../_build),)
-BIN:='$(shell cd ..; pwd)'/_build/install/default/bin/
-COQLIB:='$(shell cd ..; pwd)'/_build/install/default/lib/coq
+BIN:=$(ROOT)/_build/install/default/bin/
+COQLIB:=$(ROOT)/_build/install/default/lib/coq
else
-BIN := '$(shell cd ..; pwd)'/bin/
+BIN := $(ROOT)/bin/
COQLIB?=
ifeq ($(COQLIB),)