aboutsummaryrefslogtreecommitdiffstats
path: root/doc
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2017-01-26 10:22:28 +0100
committerMichael Schmidt <github@mschmidt.me>2017-01-26 10:22:28 +0100
commit66d4ba0f72518add12cd1cfb8ef2c40864f50bfe (patch)
treea809ea52ee03f9d491c35cf9ef9c15dfbec3878b /doc
parente7a5b00b7920ebf81591fc2f914483b6aa27269a (diff)
downloadcompcert-kvx-66d4ba0f72518add12cd1cfb8ef2c40864f50bfe.tar.gz
compcert-kvx-66d4ba0f72518add12cd1cfb8ef2c40864f50bfe.zip
describe -conf and -target
Diffstat (limited to 'doc')
-rw-r--r--doc/ccomp.111
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/ccomp.1 b/doc/ccomp.1
index 1aea4ff1..c4d214cd 100644
--- a/doc/ccomp.1
+++ b/doc/ccomp.1
@@ -47,6 +47,17 @@ Object file.
Library file.
.
.SH OPTIONS
+.SS General Options
+.INDENT 0.0
+.
+.TP
+.B \-conf <file>
+Read CompCert configuration from <file>. This takes precedence over any other specification.
+.
+.TP
+.B \-target <triple>
+Read CompCert configuration from <triple>.ini instead of using the default of compcert.ini.
+.
.SS Processing Options
.INDENT 0.0
.