diff options
Diffstat (limited to 'math/lean4/files/patch-src_bin_leanc.in')
| -rw-r--r-- | math/lean4/files/patch-src_bin_leanc.in | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/math/lean4/files/patch-src_bin_leanc.in b/math/lean4/files/patch-src_bin_leanc.in new file mode 100644 index 000000000000..6b110ae220b3 --- /dev/null +++ b/math/lean4/files/patch-src_bin_leanc.in @@ -0,0 +1,11 @@ +--- src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC ++++ src/bin/leanc.in +@@ -7,7 +7,7 @@ done + [[ "$arg" = "-c" ]] && ldflags=() + [[ "$arg" = "-v" ]] && v=1 + done +-cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) ++cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument -fPIC) + cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") + [[ $v == 1 ]] && echo $cmd + eval $cmd |