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 /flocq | |
| 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 'flocq')
0 files changed, 0 insertions, 0 deletions