summaryrefslogtreecommitdiff
path: root/Makefile.config_if_required
diff options
context:
space:
mode:
authorSébastien Hinderer <Sebastien.Hinderer@inria.fr>2021-02-01 15:37:51 +0100
committerSébastien Hinderer <Sebastien.Hinderer@inria.fr>2021-02-01 16:10:47 +0100
commit7617546ef1a240e4fe704c4b665bcbea584ef659 (patch)
tree66f0a295c3d1efc6933f779170c11545022baeb2 /Makefile.config_if_required
parentf013ea36d7a06393a61750bcc1007d2209a3b8d4 (diff)
downloadocaml-7617546ef1a240e4fe704c4b665bcbea584ef659.tar.gz
Initialize MAKECMDGOALS correctly
Diffstat (limited to 'Makefile.config_if_required')
-rw-r--r--Makefile.config_if_required4
1 files changed, 1 insertions, 3 deletions
diff --git a/Makefile.config_if_required b/Makefile.config_if_required
index cc84164bee..a25ffeb689 100644
--- a/Makefile.config_if_required
+++ b/Makefile.config_if_required
@@ -13,9 +13,7 @@
#* *
#**************************************************************************
-ifeq "$(MAKECMDGOALS)" ""
-MAKECMDGOALS += defaultentry
-endif
+MAKECMDGOALS ?= defaultentry
CLEAN_TARGET_NAMES=clean partialclean distclean