make/Init.gmk
changeset 47217 72e3ae9a25eb
parent 45822 f8fca310fb7b
child 47253 92fd0e04e0e1
--- a/make/Init.gmk	Tue Sep 12 19:03:39 2017 +0200
+++ b/make/Init.gmk	Tue Sep 12 19:03:56 2017 +0200
@@ -266,7 +266,7 @@
 	  $(ECHO) "Re-running configure using default settings"
         endif
 	( cd $(OUTPUT_ROOT) && PATH="$(ORIGINAL_PATH)" \
-	    $(BASH) $(TOPDIR)/configure $(CONFIGURE_COMMAND_LINE) )
+	    $(BASH) $(CONFIGURE_CMD) $(CONFIGURE_COMMAND_LINE) )
 
   ##############################################################################
   # The main target, for delegating into Main.gmk