diff options
author | Tavian Barnes <tavianator@tavianator.com> | 2024-05-24 08:54:57 -0400 |
---|---|---|
committer | Tavian Barnes <tavianator@tavianator.com> | 2024-05-24 08:54:57 -0400 |
commit | 64fcb1d975e8ec8ac70f7ae8add2f7499e6fe6e9 (patch) | |
tree | b5c55459e3f33f9685af2f8e063a1fcf06b88168 | |
parent | 65a7814b2dbc10ea86610092f03d0c1df95d08ad (diff) | |
download | bfs-64fcb1d975e8ec8ac70f7ae8add2f7499e6fe6e9.tar.xz |
configure: Support more standard autoconf options
-rwxr-xr-x | configure | 14 |
1 files changed, 12 insertions, 2 deletions
@@ -66,6 +66,8 @@ Packaging: --prefix=/path Set the installation prefix (default: /usr) + --mandir=/path + Set the man page directory (default: \$PREFIX/share/man) This script is a thin wrapper around a makefile-based configuration system. Any other arguments will be passed directly to the $MAKE invocation, e.g. @@ -100,9 +102,17 @@ EOF esac ;; - --prefix=*) + --prefix=*|--mandir=*) shift - set -- "$@" "PREFIX=${arg#*=}" + name="${arg#--}" + name="${name%%=*}" + NAME=$(printf '%s' "$name" | tr 'a-z-' 'A-Z_') + set -- "$@" "$NAME=${arg#*=}" + ;; + + --infodir=*|--build=*|--host=*|--target=*) + shift + printf 'warning: Ignoring option "%s"\n' "${arg%%=*}" >&2 ;; MAKE=*) |