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, 0 insertions, 11 deletions
diff --git a/math/lean4/files/patch-src_bin_leanc.in b/math/lean4/files/patch-src_bin_leanc.in deleted file mode 100644 index 6b110ae220b3..000000000000 --- a/math/lean4/files/patch-src_bin_leanc.in +++ /dev/null @@ -1,11 +0,0 @@ ---- 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 |