diff --git a/src/tools/autoconf_patch.sh b/src/tools/autoconf_patch.sh new file mode 100755 index 0000000000..f2e431a113 --- /dev/null +++ b/src/tools/autoconf_patch.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +rm -f autoconf.patch +cat > autoconf.patch <