diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-02-04 13:58:38 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-04 15:58:38 -0600 |
| commit | d89ff37c2dfbd91dd89169ad5dda06b5cc8f0a7b (patch) | |
| tree | a04312dae5b16b785e7c8c6c8ab77e4c82606f64 /configure.sh | |
| parent | c8d7db69e6b5274c21029f231a1d312518d658e7 (diff) | |
Clarifying documentation of `--static-binary` (#5844)
The documentation regarding --static-binary is improved.
Diffstat (limited to 'configure.sh')
| -rwxr-xr-x | configure.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.sh b/configure.sh index 48d1b82b2..0455e6360 100755 --- a/configure.sh +++ b/configure.sh @@ -29,7 +29,8 @@ General options; Features: The following flags enable optional features (disable with --no-<option name>). --static build static libraries and binaries [default=no] - --static-binary enable/disable static binaries + --static-binary statically link against system libraries + (must be disabled for static macOS builds) [default=yes] --proofs support for proof generation --optimized optimize the build --debug-symbols include debug symbols |