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/Core/Raux.v | |
parent | 4925303d4f8c011fbb40157cbf44e51a68f7aa2d (diff) | |
download | compcert-ebcece704b34a276fae56a546133a15f75086cdd.tar.gz compcert-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/Core/Raux.v')
0 files changed, 0 insertions, 0 deletions