make/Main.gmk
changeset 28809 6481e27e00ee
parent 28606 e4a5774f2ddd
child 28811 65cf1b4087cf
--- a/make/Main.gmk	Wed Jul 05 20:18:43 2017 +0200
+++ b/make/Main.gmk	Fri Feb 06 09:56:30 2015 +0100
@@ -553,7 +553,8 @@
         else
 	  @$(ECHO) "Re-running configure using default settings"
         endif
-	@( cd $(OUTPUT_ROOT) && $(BASH) $(TOPDIR)/configure $(CONFIGURE_COMMAND_LINE) )
+	@( cd $(OUTPUT_ROOT) && PATH="$(ORIGINAL_PATH)" \
+	    $(BASH) $(TOPDIR)/configure $(CONFIGURE_COMMAND_LINE) )
 
 ALL_TARGETS += reconfigure