diff options
| author | Daniel Dickman <didickman@gmail.com> | 2020-12-28 09:40:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-28 15:40:09 +0100 |
| commit | ebcece704b34a276fae56a546133a15f75086cdd (patch) | |
| tree | ce003dde6ef1d54ec09cc8814a285dcfe1f5b6ff /configure | |
| parent | 4925303d4f8c011fbb40157cbf44e51a68f7aa2d (diff) | |
| download | compcert-kvx-ebcece704b34a276fae56a546133a15f75086cdd.tar.gz compcert-kvx-ebcece704b34a276fae56a546133a15f75086cdd.zip | |
configure: add -mandir option (#382)
To control where man pages are installed.
The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`.
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 8 |
1 files changed, 7 insertions, 1 deletions
@@ -18,6 +18,7 @@ prefix='/usr/local' bindir='$(PREFIX)/bin' libdir='$(PREFIX)/lib/compcert' +mandir='$(PREFIX)/share/man' coqdevdir='$(PREFIX)/lib/compcert/coq' toolprefix='' target='' @@ -85,6 +86,7 @@ Options: -prefix <dir> Install in <dir>/bin and <dir>/lib/compcert -bindir <dir> Install binaries in <dir> -libdir <dir> Install libraries in <dir> + -mandir <dir> Install man pages in <dir> -coqdevdir <dir> Install Coq development (.vo files) in <dir> -toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref> -use-external-Flocq Use an already-installed Flocq library @@ -114,6 +116,8 @@ while : ; do bindir="$2"; shift;; -libdir|--libdir) libdir="$2"; shift;; + -mandir|--mandir) + mandir="$2"; shift;; -coqdevdir|--coqdevdir) coqdevdir="$2"; install_coqdev=true; shift;; -toolprefix|--toolprefix) @@ -614,7 +618,7 @@ cat > Makefile.config <<EOF PREFIX=$prefix BINDIR=$bindir LIBDIR=$libdir -MANDIR=$sharedir/man +MANDIR=$mandir SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_NATIVE_COMP=$ocaml_native_comp @@ -801,6 +805,7 @@ else bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"` libdirexp=`echo "$libdir" | sed -e "s|\\\$(PREFIX)|$prefix|"` +mandirexp=`echo "$mandir" | sed -e "s|\\\$(PREFIX)|$prefix|"` coqdevdirexp=`echo "$coqdevdir" | sed -e "s|\\\$(PREFIX)|$prefix|"` cat <<EOF @@ -826,6 +831,7 @@ CompCert configuration: Binaries installed in......... $bindirexp Runtime library provided...... $has_runtime_lib Library files installed in.... $libdirexp + Man pages installed in........ $mandirexp Standard headers provided..... $has_standard_headers Standard headers installed in. $libdirexp/include EOF |