diff options
| -rwxr-xr-x | .github/configure.sh | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/.github/configure.sh b/.github/configure.sh index e098730f..502bf5f0 100755 --- a/.github/configure.sh +++ b/.github/configure.sh @@ -2,5 +2,20 @@ . .github/configs $1 -set -x +printf "$ " + +if [ "x$CC" != "x" ]; then + printf "CC='$CC' " +fi +if [ "x$CFLAGS" != "x" ]; then + printf "CFLAGS='$CFLAGS' " +fi +if [ "x$CPPFLAGS" != "x" ]; then + printf "CPPFLAGS='$CPPFLAGS' " +fi +if [ "x$LDFLAGS" != "x" ]; then + printf "LDFLAGS='$LDFLAGS' " +fi + +echo ./configure ${CONFIGFLAGS} ./configure ${CONFIGFLAGS} |