From 2be3d97cdd76c16eb3c461cdc1e12be386271772 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 28 Sep 2021 14:14:05 +0200 Subject: [PATCH] chore: leanc: typo & minor modifications --- src/bin/leanc.in | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/bin/leanc.in b/src/bin/leanc.in index 3c0aad51b1..e6bb09797a 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -2,8 +2,9 @@ # used only for building Lean itself root=$(dirname $0) ldflags=("-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) -for arg in "@$"; do - # ccache dosn't like linker flags being passed here +for arg in "$@"; do + # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() + [[ "$arg" = "-v" ]] && set -x done -${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument +exec ${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument