Merge branch 'jk/execv-dashed-external' into maint

diff --git a/Makefile b/Makefile
index ca9f16d19a969e354990c34987414c849bbf6461..d5454ca33632f8027b06399acc56b7163074b056 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -2249,6 +2249,9 @@ endif
 ifdef GIT_PERF_MAKE_OPTS
        @echo GIT_PERF_MAKE_OPTS=\''$(subst ','\'',$(subst ','\'',$(GIT_PERF_MAKE_OPTS)))'\' >>$@+
 endif
+ifdef GIT_INTEROP_MAKE_OPTS
+       @echo GIT_INTEROP_MAKE_OPTS=\''$(subst ','\'',$(subst ','\'',$(GIT_INTEROP_MAKE_OPTS)))'\' >>$@+
+endif
 ifdef TEST_GIT_INDEX_VERSION
        @echo TEST_GIT_INDEX_VERSION=\''$(subst ','\'',$(subst ','\'',$(TEST_GIT_INDEX_VERSION)))'\' >>$@+
 endif